HoTT SQL: Proving Query Rewrites
with Univalent SQL Semantics
Shumo Chu∗

Konstantin Weitz∗

Alvin Cheung

Dan Suciu

arXiv:1607.04822v2 [] 5 Aug 2016

University of Washington, USA
{chushumo, weitzkon, akcheung, suciu}@cs.washington.edu

Abstract

act with relational database systems, only makes the task even more
difficult. As a result, while various rewrite rules have been proposed
and studied extensively in the data management research community [33, 36, 37, 44], to the best of our knowledge only the trivial ones have been formally proven to be semantically preserving.
This has unfortunately led to dire consequences as incorrect query
results have been returned from widely-used database systems due
to unsound rewrite rules, and such bugs can often go undetected for
extended periods of time [17, 43, 45].
In this paper we describe a system to formally verify the equivalence of two SQL expressions. We demonstrate its utility by proving correct a large number of query rewrite rules that have been described in the literature and are currently used in popular database
systems. We also show that, given counter examples, common mistakes made in query optimization fail to pass our formal verification, as they should. Our system shares similar high-level goals of
building formally verified systems using theorem provers and proof
assistants as recent work has demonstrated [11, 31, 32].
The biggest challenge in designing a formal verification system
for equivalence of SQL queries is choosing the right SQL semantics. Among the various features of SQL, the language uses both
set and bag semantics and switches freely between them, making
semantics definition of the language a difficult task. Although SQL
is an ANSI standard [28], the “formal” semantics defined there is of
little use for formal verification: it is loosely described in English
and has resulted in conflicting interpretations [16]. Researchers
have defined two quite different rigorous semantics of SQL. The
first comes from the formal methods community [35, 53, 54], where
SQL relations are interpreted as lists, and SQL queries as functions over lists; two queries are equivalent if they return lists that
are equal up to element permutation (under bag semantics) or up
to element permutation and duplicate elimination (under set semantics). The problem with this semantics is that even the simplest equivalences require lengthy proofs in order to reason about
order-independence or duplicate elimination, and these proofs become huge when applied to rewrites found in real-world optimizations. The second semantics comes from the database theory community and uses only set semantics [1, 6, 38]. This line of work
has led to theoretical results characterizing languages for which
query equivalence is decidable (and often fully characterizing the
complexity of the equivalence problem), and separating them from
richer languages where equivalence is undecidable [8, 19, 42, 51].
For example, equivalence is decidable (and ΠP
2 -complete for a
fixed database schema [51], and coNEXPTIME-complete in general [19]) for conjunctive queries with safe negation, but undecidable for conjunctive queries with unsafe negation. Unfortunately,
this approach is of limited use in practice, because most query optimization rules use features that places them in the undecidable
language fragments.
This paper contributes a new semantics for SQL that is both
simple and allows simple proofs of query equivalence. We then

Every database system contains a query optimizer that performs
query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes
from the intricacies and rich features of query languages, which
makes reasoning about rewrite rules difficult. In this paper, we
propose a machine-checkable denotational semantics for SQL, the
de facto language for relational database, for rigorously validating
rewrite rules. Unlike previously proposed semantics that are either
non-mechanized or only cover a small amount of SQL language
features, our semantics covers all major features of SQL, including
bags, correlated subqueries, aggregation, and indexes. Our mechanized semantics, called HoTT SQL, is based on K-Relations and
homotopy type theory, where we denote relations as mathematical functions from tuples to univalent types. We have implemented
HoTT SQL in Coq, which takes only fewer than 300 lines of code
and have proved a wide range of SQL rewrite rules, including
those from database research literature (e.g., magic set rewrites)
and real-world query optimizers (e.g., subquery elimination). Several of these rewrite rules have never been previously proven correct. In addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using
HoTT SQL for conjunctive queries: a well-studied decidable fragment of SQL that encompasses many real-world queries.

1.

Introduction

From purchasing plane tickets to browsing social networking websites, we interact with database systems on a daily basis. Every
database system consists of a query optimizer that takes in an input
query and determines the best program, also called a query plan,
to execute in order to retrieve the desired data. Query optimizers
typically consists of two components: a query plan enumerator that
generates query plans that are semantically equivalent to the input
query, and a plan selector that chooses the optimal plan from the
enumerated ones to execute based on a cost model.
The key idea behind plan enumeration is to apply rewrite rules
that transform a given query plan into another one, hopefully one
with a lower cost. While numerous plan rewrite rules have been
proposed and implemented, unfortunately designing such rules remains a highly challenging task. For one, rewrite rules need to be
semantically preserving, i.e., if a rule transforms query plan Q into
Q0 , then the results (i.e., the relation) returned from executing Q
must be the same as those returned from Q0 , and this has to hold
for all possible input database schemas and instances. Obviously,
establishing such proof for any non-trivial query rewrite rule is not
an easy task.
Coupled with that, the rich language constructs and subtle semantics of SQL, the de facto programming language used to inter∗ These

authors contributed equally to this work.

1

2016/8/9

Rewrite Rule:

demonstrates its effectiveness by proving the correctness of various
powerful query optimization rules described in the literature.
Our semantics consists of two non-trivial generalizations of
K-relations. K-relations were introduced by Green et al. in the
database theory community [23], and represent a relation as mathematical function that takes as input a tuple and returns its multiplicity in the relation, with 0 meaning that the tuple does not exist in the relation. A K-relation is required to have finite support,
meaning that only a finite set of tuples have multiplicity > 0. Krelations greatly simplify reasoning about SQL: under set semantics, a relation is simply a function that returns 0 or 1 (i.e., a Boolean
value), while under bag semantics it returns a natural number (i.e.,
a tuple’s multiplicity). Database operations such as join or union
become arithmetic operations on the corresponding multiplicities:
join becomes multiplication, union becomes addition. Determining
the equivalence of a rewrite rule that transforms a query Q into another query Q0 reduces to checking the equivalence of the functions
they denote. For example, proving that the join operation is associative reduces to proving that multiplication is associative. As we
will show, reasoning about functions over cardinals is much easier
than writing inductive proofs on data structures such as lists.
However, K-relations as defined by [23] are difficult to use in
proof assistants, because one needs to prove for every SQL expression under consideration that the K-relation it returns has finite
support: this is easy with pen-and-paper, but very hard to encode
for a proof assistant. Without a guarantee of finite support, some
operations are undefined, for example projection on an attribute requires infinite summation. Our first generalization of K-relations
is to drop the finite support requirement, and meanwhile allow the
multiplicity of a tuple to be any cardinal number as opposed to a
(finite) natural number. Then the possibly infinite sum corresponding to a projection is well defined. With this change, SQL queries
are interpreted over finite and infinite bags, where some tuples may
have infinite multiplicities. To the best of our knowledge, ours is
the first SQL semantics that interprets relations as both finite and
infinite; we discuss some implications in Sec. 7.
Our second generalization of K-relations is to replace cardinal numbers with univalent types. Homotopy Type Theory
(HoTT) [46] has been introduced recently as a generalization of
classical type theory by adding membership and equality proofs. A
univalent type is a cardinal number (finite of infinite) together with
the ability to prove equality.
To summarize, we define a SQL semantics where a relation is
interpreted as a function mapping each tuple to a univalent type,
whose cardinality represents the multiplicity of the tuple in the relation, and a SQL query is interpreted as a function from input relations to an output relation. We call the SQL language with this
particular semantics HoTT SQL. Our language covers all major
features of SQL. In addition, since univalent types have been integrated into the Coq proof assistant, we leverage that implementation to prove equivalences of SQL expressions.
To demonstrate the effectiveness of HoTT SQL, we implemented a new system called D OP C ERT (Database OPtimizations
CERTified) for proving equivalence of SQL rewrite rules. We
have used D OP C ERT to prove many well-known and commonlyused rewrite rules from the data management research literature,
many of which have never been formally proven correct before:
aggregates [9, 30], magic sets rewriting [2], query rewriting using indexes [49], and equivalence of conjunctive queries [1]. All
our proofs require at most a few dozens lines of Coq code using
D OP C ERT, as shown in Fig. 8. All definitions and proofs presented
in this paper are open-source and available online.1
In summary, this paper makes the following contributions:

SELECT * FROM (R UNION ALL S) WHERE b

≡

(SELECT * FROM R WHERE b) UNION ALL (SELECT * FROM S WHERE b)
HoTT SQL Denotation:
⇒λ t . (JRK t + JSK t) × JbK t ≡ λ t . JRK t × JbK t + JSK t × JbK t
HoTT SQL Proof: Apply distributivity of × over +.

Figure 1. Proving a rewrite rule using HoTT SQL. Recall that
UNION ALL means bag-union in SQL, which in HoTT SQL is translated to addition of tuple multiplicities in the two input relations.
• We present HoTT SQL, a (large fragment) of SQL whose se-

mantics generalizes K-relations to infinite relations and univalent types. The goal of this semantics is to enable easy proofs
for the equivalence of query rewrite rules. (Sec. 3.)
• We prove a wide variety of well-known and widely-used SQL

rewrite rules, where many of them have not be formally proven
before; each proof require at most a few dozens lines of Coq
code using D OP C ERT. (Sec. 4.)
• We implement D OP C ERT, a new system written in Coq for

checking the equivalence of SQL rewrite rules. D OP C ERT
comes with a number of heuristic tactics for deciding the equivalence of arbitrary rewrite rules, and a fully automated procedure for deciding rewrite rules involving conjunctive queries,
where conjunctive queries represent a fragment of SQL where
equivalence is decidable. (Sec. 5.)
The rest of this paper is organized as follows. In Sec. 2, we
given an overview and motivation for a new semantics for SQL.
We then introduce HoTT SQL in Sec. 3, its semantics in Sec. 4,
and demonstrate our results in Sec. 5. Related work is presented
in Sec. 6. We include some discussion in Sec. 7 and conclude in
Sec. 8.

2.

Overview

SQL The basic datatype in SQL is a relation, which has a schema
(a relation name R plus attribute names σ), and an instance (a bag
of tuples). A SQL query maps one or more input relations to a
(nameless) output relation. For example, if a relation with schema
R(a, b) has instance {(1, 40), (2, 40), (2, 50)} then the SQL query
Q1:SELECT a FROM R
returns the bag {1, 2, 2}.
SQL freely mixes set and bag semantics, where a set is simply a
bag without duplicates and uses the distinct keyword to remove
duplicates. For example, the query:
Q2:SELECT DISTINCT a FROM R
returns the set {1, 2}.
List Semantics Previous approaches to mechanizing formal proofs
of SQL query equivalences represent bags as list [35, 53, 54]. Every SQL query admits a natural interpretation over lists, using a
recursive definition [7]. To prove that two queries are equivalent,
one uses their inductive definition on lists, and proves that the two
results are equal up to element reordering and duplicate elimination
(for set semantics).
The main challenges in this approach are coming up with the
induction hypothesis, and dealing with list equivalence under permutation and duplicate elimination. Inductive proofs quickly grow
in complexity, even for simple query equivalences. Consider the
following query:

1 http://dopcert.cs.washington.edu

Q3:SELECT DISTINCT x.a FROM R AS x, R AS y WHERE x.a = y.a

2

2016/8/9

Rewrite Rule:

Q3 is equivalent to Q2, because it performs a redundant self-join:
the inductive proof of their equivalence is quite complex, and has,
to the best of our knowledge, not been done formally before. A
much simpler rewrite rule, the commutativity of selection, requires
65 lines of Coq proof in prior work [35], and only 10 lines of Coq
proof in our semantics. Powerful database query optimizations,
such as magic sets rewrites and conjunctive query equivalences,
are based on generalizations of redundant self-joins elimination
like Q2 ≡ Q3, but significantly more complex (see Sec. 5), and
inductive proofs become impractical. This motivated us to consider
a different semantics; we do not use list semantics in this paper.

SELECT DISTINCT x.a FROM R AS x, R AS y WHERE x.a = y.a

≡

SELECT DISTINCT a FROM R
Equational HoTT SQL Proof:

⇒λ t .

X
t1 ,t2

λt.

X
t1 ,t2

K-Relation SQL Semantics An alternative approach introduced
in [23] is to represent relations as functions that map every tuple
to a value that indicates how many times it appears in the relation.
If the relation is a bag, then the function returns a natural number,
and if it is a set then it returns a value in {0, 1}. More generally, a
commutative semi-ring is a structure K = (K, +, ×, 0, 1) where
both (K, +, 0) and (K, ×, 1) are commutative monoids, and ×
distributes over +. For a fixed set of attributes σ, denote Tuple(σ)
the type of tuples with attributes σ. A K-relation [23] is a function:

(t = JaK t1 ) × (JaK t1 = JaK t2 ) × JRK t1 × JRK t2 ≡
(t = JaK t1 ) × (t = JaK t2 ) × JRK t1 × JRK t2 ≡

X
X
λt. (
(t = JaK t1 ) × JRK t1 ) × (
(t = JaK t2 ) × JRK t2 ) ≡
t1

λt.

X
t1

t2

(t = JaK t1 ) × JRK t1

We used the following semi-ring identities:

JRK :Tuple σ → K

X

with finite support, meaning that the set {t | JRK t 6= 0} is finite.
A bag is an N-relation, and a set is a B-relation. All relational
operators are expressed in terms of the semi-ring operations, for
example:

(a = b) × (b = c) ≡(a = b) × (a = c)
X
X
E1 (t1 ) × E2 (t2 ) ≡
E1 (t1 ) ×
E2 (t2 )

t1 ,t2

t1

t2

kn × nk ≡ knk
Deductive HoTT SQL Proof:
⇒ ∀ t.∃t0 (JaK t0 = t) ∧ JRK t0 ↔

JR UNION ALL SK = λ t . JRK t + JSK t
JSELECT * FROM R, SK = λ (t1 , t2 ) . JRK t1 × JSK t2

∃t1 ,t2 (JaK t1 = t) ∧ JRK t1 ∧ JRK t2 ∧ (JaK t1 = JaK t2 )

Then case split on ↔. Case →: instantiate both t1 and t2 with t0 , then
apply hypotheses. Case ←: instantiate t0 with t1 , then apply hypotheses.

JSELECT * FROM R WHERE bK = λ t . JRK t × JbK t
X
JSELECT x.a FROM RK = λ t .
(t = JaK t0 ) × JRK t0

Figure 2. The proof of equivalence Q2 ≡ Q3.

t0 ∈Tuple σ

JSELECT DISTINCT * FROM RK = λ t . kJRK tk

0, 1 is the unit type 1, multiplication is the product type ×, addition
is the sum type +, infinite summation is the dependent product
type Σ, and truncation is the squash type k.k. Homotopy types
generalize natural numbers and their semiring operations, and is
now well integrated with automated proof assistants like Coq 2 . As
we show in the rest of this paper, the equivalence proofs retain the
simplicity of N-relations and can be easily mechanized, but without
the need to prove finite support.
In addition, homotopy type theory unifies squash type and
proposition. Using the fact that propositions as types in homotopy type theory [46, Ch 1.11], in order to prove the equivalence of
two squash types, kpk and kqk, it is sufficient to just prove the biimplication (p ↔ q), which is arguably easier in Coq. For example,
transforming the equivalence proof of Figure 2 to bi-implication
would not require a series of equational rewriting using semi-ring
identities any more, which is complicated because it is under the
variable bindings of Σ. The bi-implication can be proved in Coq by
deduction easily.
The queries of the above rewrite rule fall in the well studied
category of conjunctive queries, for which equality is decidable
(equality between arbitrary SQL queries is undecidable). Using
Coq’s support for automating deductive reasoning (with Ltac), we
have implemented a decision procedure for the equality of conjunctive queries, the aforementioned rewrite rule can thus be proven in
one line of Coq code.

where, for any predicate b: JbK t = 1 if the predicate holds on t, and
JbK t = 0 otherwise. The function k k is defined as kxk = 0 when
x = 0, and kxk = 1 otherwise (see Subsec. 3.4). The projection
JaK t0 returns the attribute a of the tuple t0 , while equality (x = y)
is interpreted as 0 when x 6= y and 1 otherwise.
To prove that two SQL queries are equal one has to prove that
two semi-ring expressions are equal. For example, Fig. 1 shows
how we can prove that selections distribute over unions, by reducing it to the distributivity of × over +, while Fig. 2 shows the proof
of the equivalence for Q2 ≡ Q3.
Notice that the definition of projection requires that the relation
has finite support; otherwise, the summation is over an infinite
set and is undefined in N. This creates a major problem for our
equivalence proofs, since we need to prove, for each intermediate
result of a SQL query, that it returns a relation with finite support.
This adds significant complexity to the otherwise simple proofs of
equivalence.
HoTT SQL Semantics To handle this challenge, our semantics
generalizes K-Relation in two ways: we no longer require relations
to have finite support, and we allow the multiplicity of a tuple to be
an arbitrary cardinality (possibly infinite). More precisely, in our
semantics a relation is interpreted as a function:
Tuple σ → U

3. HoTT SQL and Its Semantics

where U is the class of homotopy types. We call such a relation a
HoTT-relation. A homotopy type n ∈ U is an ordinary type with
the ability to prove membership and equality between types.
Homotopy types form a commutative semi-ring and can well
represent cardinals. Cardinal number 0 is the empty homotopy type

In this section, we present HoTT SQL, a SQL-like language for
expressing rewrite rules. To simplify discussion, we first describe
2 After

3

adding the Univalence Axiom to Coq’s underlying type theory.

2016/8/9

τ ∈ Type
JintK
JboolK
JstringK
...

::=
::=
::=
::=

int | bool | string | . . .
Z
B
String

σ ∈ Schema

::=
|
|

empty
leaf τ
node σ1 σ2

Tuple empty
Tuple (node σ1 σ2 )
Tuple (leaf τ )

::=
::=
::=

Unit
Tuple σ1 × Tuple σ2
Jτ K

The tuple type in HoTT SQL is defined as a dependent type on
a schema. As shown in Figure 3, a tuple is an nested pair with the
identical structure as its schema. Given a schema s, if s is the empty
schema, then the (only) instance of Tuple empty is Unit (i.e.,
empty) tuple. Otherwise, if s is a leaf node in the schema tree with
type τ , then a tuple is simply a value of the type Jτ K. Finally, if s is
recursively defined using two schemas s1 and s2 , then the resulting
tuple is an instance of a product type Tuple(s1 ) × Tuple(s2 ).
As an illustration, Figure 4 shows a tuple t and its schema σ,
where σ = (node (leaf Int) (node (leaf Int) (leaf Int)))
and t has the nested pair type (String×(Z×B)). To access an element from a tuple, HoTT SQL uses path expressions with selectors
Left and Right. For instance, the path Left.Right retrieves the
value 52 from the tuple t in Figure 3. As will be shown in Sec. 4,
path expressions will be denoted to standard pair operations, i.e.,
Left will be denoted to “.1”, which returns the first element from
a pair, and Left will be denoted to “.2”, which returns the second.
Such expressions can be composed to retrieve nested pair types. For
instance, Left.Right will be denoted to “.1.2”, thus it retrieves 52
from t in Figure 3.

Figure 3. Data Model of HoTT SQL

σ : Schema

=

Tuple σ
t : Tuple σ

=
=

string

int

node (leaf int)
(node (leaf int)
(leaf bool))
String × (Z × B)
(“Bob00 , (52, true))

Relation In HoTT SQL a relation is modeled as a function from
tuples to homotopy types called HoTT-relations, Tuple σ → U , as
already discussed in Sec. 2; we define homotopy types shortly.
Discussion We briefly comment on our choice of data model.
There are two approaches to defining tuples in database theory [1]:
the named approach and unnamed approach. We chose an unnamed
approach, because it avoids name collisions, and because proof
assistants like Coq can decide schema equivalence of unnamed
schemas based on structural equality. Previous work [35] adopted
an unnamed approach as well, for the same reason. Our choice for
representing tuples as trees, rather than as ordered lists, is nonstandard: we do this in order to allow our language to express
generic rewrite rules, without specifying a particular schema for
the input relations, see Sec. 3.3.
Finally, we note that, in our model, a tuple is a dependent type,
which depends on its schema. We use dependent types to ensure
that a tuple, which is a nested pair, must have the same structure as
its schema, which is a binary tree, by construction. This allows us
to denote a path expression (composed by Left, Right) to a series
of corresponding pair operations (composed by “.1”, “.2”) easily.

bool

Figure 4. An Example of HoTT SQL Schema and Tuple
how relational data structures are modeled in Section 3.1. We then
describe HoTT SQL, a language built on top of our relational data
structures that covers all major features of SQL, in Section 3.2.
Next, we define U NI N OMIAL, the formal expressions into which
HoTT SQL is translated, in Section 3.4.
3.1

Data Model

We first describe how schemas for relations and tuples are modeled
in HoTT SQL. Both of these foundational concepts from relational
theory [13] are what HoTT SQL uses to build upon.
Schema and Tuple We briefly review the standard SQL definitions of a schema and a tuple. Conceptually, a database schema is
an unordered bag of (n, τ ) pairs, where n is an attribute name, and
τ is the type of the attribute. For example, the schema of a table
containing personal information might be:

3.2 HoTT SQL: A SQL-like Query Language
We now describe HoTT SQL, our source language used to express
rewrite rules. Figure 5 defines the syntax of HoTT SQL. We divide
the language constructs of HoTT SQL into four categories: queries,
predicates, expressions, and projections.

{(Name, string), (Age, int), (Married, bool)}

Queries A query takes in relation(s) and outputs another relation.
The input to a query can be a base relation (called a T able in Figure 5) or other queries, including projections, cross product, selections, bag-wise operations (UNION ALL and EXCEPT), and finally
conversion to sets (DISTINCT).

A database tuple is a collection of values that conform to a given
schema. For example, the following is a tuple with the aforementioned schema:
{Name : “Bob”; Age : 52; Married : true}

Predicates Predicates are used as part of selections (i.e., filtering
of tuples) in queries. Given a tuple t, predicates return a Boolean
value to indicate whether t should be retained in the output relation.

Attributes from tuples are accessed using record syntax. For
instance t.Name returns “Bob” where t refers to the tuple above.
As shown in Figure 3, we assume there exists a set of SQL types
Type, which can be denoted into types in Coq.
In HoTT SQL, we define schemas and tuples as follows. A
schema is modeled as a collection of types organized in a binary
tree, with each type corresponding to an attribute. As shown in Figure 3, a schema can be constructed from the empty schema, an
individual type τ , or recursively from two schema nodes s1 and s2 ,
corresponding to the branches of the subtree. As we will see, this
organization is beneficial in both writing HoTT SQL rewrite rules
and also reasoning about the equivalence of schemas.

Expressions Expressions are used both in predicates and projections, and they evaluate to values (e.g., of type Z, B, String,
etc). Expression includes conversions from projection to expression (P2E p), uninterpreted functions on expressions, aggregators
of a query, and casts of an expression (CASTEXPR p e).
P2E p converts a projection p into an expression. For example,
P2E a = P2E b is an equality predicate on attribute a and attribute b,
where P2E a and P2E b are the expressions representing attribute a
and b. As shown next, we use a projection to represent an attribute.

4

2016/8/9

Uninterpreted functions of expressions f (e1 , . . . , en ) are used
to represent arithmetic operations on expressions such as addition,
multiplication, division, mode, and constants (which are nullary
uninterpreted functions).
CASTEXPR is a special construct that is used to represent castings of meta-variables to express generic query rewrite rules.
A comprehensive discussion of meta-variables can be found in
Sec. 3.3. A normal (non-generic) query would not need CASTEXPR.

q ∈ Query

b ∈ Predicate

Projections When applied to a relation, projections denote a subset of attributes to be returned. A projection is defined to be a tuple to tuple function. It can be the identity function (*), or return
the subtree denoted by any of the path expressions as discussed
in Sec. 3.1, such as returning the left (Left) or right (Right) subtree
of the tuple. Any empty tuple can also be produced using empty.
Multiple projections can be composed using “.”. Two projections
p1 and p2 can be applied to the input tuple separately with the results combined together using “,”. E2P p is used to convert a projection to an expression. Below are examples of HoTT SQL query
using projections:

e ∈ Expression
p ∈ Projection

::=
|
|
|
|
|
|
::=
|
|
|
::=
|
|
::=
|
|
|

Table
SELECT p q
FROM q1 , . . . , qn
q WHERE p
q1 UNION ALL q2
q1 EXCEPT q2
DISTINCT q
e1 = e2
NOT b | b1 AND b2 | b1 OR b2 | true | false
CASTPRED p b
EXISTS q
P2E p
f (e1 , . . . , en ) | agg(q)
CASTEXPR p e
* | Left | Right | Empty
p1 . p 2
p1 , p2
E2P e

Figure 5. Syntax of HoTT SQL
HoTT SQL
q1
SELECT Left.* FROM R, S
q2
SELECT Right.* FROM R, S
Since our data model is a tree, it is very convenient to use
q3
SELECT Right.p FROM R, S
a meta-variable p to navigate to any leaf (corresponding to an
q4
SELECT Left.p1 , Right.p2
attribute), and it also easy to concatenate two schemas using the
FROM R, S
q5
SELECT E2P add(P2E p1 , P2E p2 ) node constructor; in contrast, a data model based on ordered lists
would make the combination of navigation and concatenation more
FROM R
difficult.
In q1 , we compose the path expressions Left and * to represent
Second, we explain the functions CASTPRED and CASTEXPR
projecting all attributes of R from a tuple that is in the result of R ./
in HoTT SQL with another example. Consider the rewrite rule (to
3
S . In q3 , we compose Right and k to project to a single attribute
be presented in Sec. 5.1.1) for pushing down selection predicates,
from S. The variable k is a projection to a singleton tuple, which
written informally as:
is the way to represent attributes in our semantics. In q4 , we are
SELECT * FROM R, (SELECT * FROM S WHERE b) ≡
projecting one attribute p1 from R, and another attribute p2 from
SELECT * FROM R, S WHERE b
S using the projection combinator “,”. In q5 , to represent p1 + p2 ,
we first convert attributes (p1 , p2 ) to expressions (P2E p1 , P2E p2 ),
In this rule, b is a meta-variable that ranges over all possible
then use an uninterpreted function add to represent addition, and
Boolean predicates. In standard SQL, the two occurrences of b
are simply identical expressions, but in HoTT SQL the second
cast that back to a projection using E2P .
occurrence is in a environment that consists of the schemas of
both R and S. In HoTT SQL, this is done rigorously using the
3.3 Expressing Rewrite Rules
CASTPRED construct:
HoTT SQL is a language for expressing query rewrite rules, and
SELECT * FROM R, (SELECT * FROM S WHERE b) ≡
each such rule needs to hold over all relations (i.e., both sides
SELECT * FROM R, S WHERE (CASTPRED Right b)
of each rule need to return the same relation for all schemas and
instances, as discussed in Sec. 2), and likewise for predicates and
The expression CASTPRED Right b is function composition: it
expressions. To facilitate that, HoTT SQL allows users to declare
applies Right first, to obtain the schema of R, then evaluates the
meta-variables for queries, predicates, and expressions, and uses
predicate b on the result.
two functions CASTPRED and CASTEXPR , as we illustrate next.
Requiring explicit casts is an important feature of HoTT SQL:
First, consider meta-variables. Referring to Figure 1, the base
doing so ensures that rewrite rules are only applicable in situations
tables R and S are meta-variables that can be quantified over all
where they are valid. In the example above, the rule is only valid
possible relations, and b is a meta-variable ranging over predicates.
for all predicates b where b refers only to attributes in S, and the
For another example, consider the rewrite rule in Fig. 2: we want to
cast operation makes that explicit. The CASTEXPR construct works
say that the rule holds for any relation R with a schema having an
similarly for expressions.
attribute a. We express this in HoTT SQL by using a meta-variable
p instead of the attribute a:
3.4 UniNomials
DISTINCT SELECT Left.p FROM R, R
The interpretation of a HoTT SQL expression is a formal expresSQL
SELECT R.∗ FROM R, S
SELECT S.∗ FROM R, S
SELECT S.p FROM R, S
SELECT R.p1 , S.p2
FROM R, S
SELECT p1 + p2 FROM R

WHERE P2E Left.p = P2E Right.p

sion over U NI N OMIAL, which is an algebra of univalent types.

≡ DISTINCT SELECT p FROM R

Definition 3.1. U NI N OMIAL, the algebra
of Univalent Types, conP
sists of (U, 0, 1, +, ×, · → 0, k·k , ), where:

3 Technically

./ denotes natural join in relational theory [13]. However,
since HoTT SQL schemas are unnamed, there are no shared names between
schemas, and thus natural joins are equivalent to cross products. Hence, we
use ./ for cross product of relations to distinguish it from Cartesian product
of types (×) to be discussed in Sec. 3.4.

• (U, 0, 1, +, ×) forms a semi-ring, where U is the universe of

univalent types, 0, 1 are the empty and singleton types, and
+, × are binary operations U × U → U: n1 + n2 , is the direct
sum, and n1 × n2 is the Cartesian product.

5

2016/8/9

• · → 0, k·k are derived unary operations U → U, where

SELECT ∗ FROM R1 WHERE
-- predicate in q2 : R2 .b = R1 .a
EXISTS SELECT ∗ FROM R2 WHERE right.p2 =left.p1 AND
-- predicate in q3 : R3 .c=R2 .b
EXISTS SELECT ∗ FROM R3
WHERE right.p3 =left.right.p2

(0 → 0) = 1 and (n → 0) = 0 when n 6= 0, and
knk
P = (n → 0) → 0.
P
•
: (A → U) → U is the infinitary operation:
f is the
direct sum of the set of types {f (a) | a ∈ A}.
Following standard notation [46], we say that the homotopy
type n inhabits some universe U. The base cases of n come from the
denotation of HoTT-Relation and equality of two tuples (In HoTT,
propositions are squash types, which are 0 or 1 [46, Ch 1.11]).
The denotation of HoTT SQL will be shown Section 4. There are 5
type-theoretic operations on U:

Query
init
q1
q2
q3

Cartesian product (×) Cartesian product of univalent types is
analogously the same concept as the Cartesian product of two sets.
For A, B : U, the cardinality of A × B is the cardinality of A
multiplied by the cardinality of B. For example, we denote the
cross product of two HoTT-Relations using the Cartesian product
of univalent types:

Disjoint union (+) Disjoint union on univalent types is analogously the same concept as union on two disjoint sets. For A, B :
U, the cardinality of A + B is the cardinality of A adding the cardinality of B. For example, UNION ALL denotes to +:
JR1 UNION ALL R2 K , λ t. (JR1 K t) + (JR2 K t)
In SQL, UNION ALL means bag semantic union of two relations.
Thus a tuple t ∈ R1 UNION ALL R2 has a cardinality of its
cardinality in R1 (JR1 K t) added by its cardinality in R2 (JR2 K t).
We also denote logical OR of two predicates using +. A + B is
corresponded type-theoretic operation of logical OR if A and B are
squash types (recall that squash types are 0 or 1 [46, Ch 1.11]).

Negation (n → 0) If n is a squash type, n → 0 is the negation of
n. We have 0 → 0 = 1 and 1 → 0 = 0. Negation is used to denote
negating a predicate and to denote EXCEPT . For example, EXCEPT
is used to denote negation:
JR1 EXCEPT R2 K , λ t. (JR1 K t) × (kJR2 K tk → 0)

A tuple t ∈ R1 EXCEPT R2 retains its multiplicity in R1
if its multiplicity in R2 is not 0 (since if JR2 K t 6= 0, then
kJR2 K tk → 0 = 1).
P
P
Summation ( ) Given
x:A B(x) is a
P A : U and B : A → U ,
dependent pair type
is used to denote projection. For example:

t0 :Tuple σR

JkK t = t × JRK t

Context schema
Γ0 =empty
Γ1 =node Γ0 σR1
Γ2 =node Γ1 σR2
Γ3 =node Γ2 σR3

Denotation of HoTT SQL

In this section we define the denotational semantics of HoTT SQL.
We first discuss the translation of HoTT SQL constructs into U NI N OMIAL. Then, in Sec. 4.2, we describe how advanced features of
SQL (such as integrity constraints and indexes) can be expressed
using HoTT SQL and subsequently translated.
Figure 7 shows the translation of HoTT SQL to U NI N OMIAL.
The translation rules make use of contexts. A context schema Γ is a
schema (see the definition of Schema in Fig. 3); a context g is a tuple
of type Tuple Γ associated to that schema. Intuitively, the context
consists of the concatenation of all tuple variables occurring in a
surrounding scope.
For example, consider the HoTT SQL query with correlated
subqueries in Figure 4 where path expressions are used to refer
to relations in predicates, as discussed in Sec. 3.1. As in standard SQL, evaluation proceeds from the outermost to the innermost
query, starting with query q1 . After the FROM clause in q1 is processed, the context consists of R1 ’s schema (σR1 ), which is then
passed to the query q2 . In turn, q2 then processes its FROM clause,
and appends the schema of R2 to the context (node σR1 σR2 ), and
this context is used to evaluate the path expression q2 ’s predicate
(right.k = left.k, i.e., R1 .k = R2 .k), and similarly when q3
evaluates its predicate.
In our system, contexts are implemented as tuples. To make
passing of contexts explicit, in the following, each HoTT SQL
construct takes in a context tuple (represented by Tuple Γ), and
is translated to functions that take in both a tuple (t) and a context
tuple (g).

JDISTINCT RK , λ t. kJRK tk
For a tuple t ∈ DISTINCT R, its cardinality equals to 1 if its
cardinality in R is non-zero and equals to 0 otherwise. This is
exactly kJRK tk.

JSELECT k FROM RK , λ t.

q3

For a tuple t in the result of this projection query, its cardinality
is the summation of the cardinalities of all tuples of schema σA
that also has the same value on column k with t. Here kJkK t0 = tk
equals to 1 if t and t0 have same value on k, otherwise it equals to
0. Unlike K-Relations, using univalent types allow us to support
summation over an infinite domain and evaluate expressions such
as the projection described above.
In general, proving rewrite rules in U NI N OMIAL enables us
to use powerful automatic proving techniques such as associativecommutative term rewriting in semi-ring structures (recall that U
is a semi-ring) similar to the ring tactic [3] and Nelson-Oppen
algorithm on congruence closure [39]. Both of which mitigate our
proof burden.

4.

Squash (knk) Squash is a type-theoretic operation that truncates
a univalent type to 0 or 1. For A : U, kAk = 0 if A’s cardinality is
zero and kAk = 1 otherwise. An example of using squash types
is in denoting DISTINCT (DISTINCT means removing duplicated
tuples in SQL, i.e., converting a bag to a set):

0

q2

Figure 6. Using Contexts in Evaluating Correlated Subqueries

JR1 ./ R2 K , λ t. (JR1 K t.1) × (JR2 K t.2)
The result of R1 ./ R2 is a HoTT-Relation with type Tuple σR1 ./R2
→ U. For every tuple t ∈ R1 ./ R2 , its cardinality equals to the
cardinality of t’s left sub-tuple (t.1) in R1 (JR1 K t.1) multiplied by
the cardinality of t’s right sub-tuple (t.2) in R2 (JR2 K t.2).

X

q1

4.1

Denoting Basic HoTTSQL Constructs

Queries A query q is denoted to a function from q’s context tuple
(of type Tuple Γ) to a HoTT-Relation (of type Tuple σ → U ):

0

JΓ ` q : σK : T uple Γ → T uple σ → U
6

2016/8/9

JΓ ` q : σK : Tuple Γ → Tuple σ → U
JΓ ` table : σK
JΓ ` SELECT p q : σK
JΓ ` FROM q1 , q2 : node σ1 σ2 K
JΓ ` FROM q : σK
JΓ ` q WHERE b : σK
JΓ ` q1 UNION ALL q2 : σK
JΓ ` q1 EXCEPT q2 : σK
JΓ ` DISTINCT q : σK

,
,
,
,
,
,
,
,

λg
λg
λg
λg
λg
λg
λg
λg

(* Query *)
t. JtableK t
P
0
0
0
0
t.
t0 :Tuple σ 0 (Jp : node Γ σ ⇒ σK (g, t ) = t) × JΓ ` q : σ K g t
t. JΓ ` q1 : σ1 K g t.1 × JΓ ` q2 : σ2 K g t.2
t. JΓ ` q : σK g t
t. JΓ ` q : σK g t × Jnode Γ σ ` bK (g, t)
t. JΓ ` q1 : σK g t + JΓ ` q2 : σK g t
t. JΓ ` q1 : σK g t × ((JΓ ` q2 : σK g t) → 0)
t. kJΓ ` q : σK g tk

JΓ ` bK : Tuple Γ → U
JΓ ` e1 = e2 K
JΓ ` b1 AND b2 K
JΓ ` b1 OR b2 K
JΓ ` NOT bK
JΓ ` EXISTS qK

JΓ ` FALSEK
JΓ ` TRUEK
JΓ ` CASTPRED p bK

(* P redicate *)
,
,
,
,
,
,
,
,

λ g. (JΓ ` e1 : τ K g = JΓ ` e2 : τ K g)
λ g. JΓ ` b1 K g × JΓ ` b2 K g
λ g. kJΓ ` b1 K g + JΓ ` b2 K gk
λ g. (JΓ ` bK g) → 0
P
λ g.
t:Tuple σ JΓ ` q : σK g t
λ g. 0
λ g. 1
λ g. JΓ0 ` bK (Jp : Γ ⇒ Γ0 K g)

JΓ ` e : τ K : Tuple Γ → Jτ K
JΓ ` P2E p : τ K
JΓ ` f (e1 , . . .) : τ K
JΓ ` agg(q) : τ 0 K
JΓ ` CASTEXPR p e : τ K

(* Expression *)
,
,
,
,

λ g. Jp : Γ ⇒ leaf τ K g
λ g. Jf K(JΓ ` e1 : τ1 K g, . . .)
λ g. JaggK (JΓ ` q : leaf τ K g)
λ g. JΓ0 ` e : τ K (Jc : Γ ⇒ Γ0 K g)

Jp : Γ ⇒ Γ0 K : Tuple Γ → Tuple Γ0
J∗ : Γ ⇒ ΓK
JLeft : node Γ0 Γ1 ⇒ Γ0 K
JRight : node Γ0 Γ1 ⇒ Γ1 K
JEmpty : Γ ⇒ emptyK
Jp1 . p2 : Γ ⇒ Γ00 K
Jp1 , p2 : Γ ⇒ node Γ0 Γ1 K
JE2P e : Γ ⇒ leaf τ K

,
,
,
,
,
,
,

(* P rojection *)
λ g. g
λ g. g.1
λ g. g.2
λ g. unit
λ g. Jp2 : Γ0 ⇒ Γ00 K (Jp1 : Γ ⇒ Γ0 K g)
λ g. (Jp1 : Γ ⇒ Γ0 K g, Jp2 : Γ ⇒ Γ1 K g)
λ g. JΓ ` e : τ K g

Figure 7. Denotational Semantics of HoTT SQL
and the combination is easily accomplished as g, the context tuple,
has schema Γ.
UNION ALL, EXCEPT, and DISTINCT are denoted using +, negation (n → 0) and merely (knk) on univalent types as shown in
Section 3.4.

The FROM clause is recursively denoted to a series of cross
products of HoTT-Relations. Each cross product is denoted using
× as shown in Section 3.4. For example:
JΓ ` FROM q1 , q2 : σK
λ g t. (JΓ ` q1 : σK g t.1) × (JΓ ` q2 : σK g t.2)

,

Predicates A predicate b is denoted to a function from a tuple (of
type Tuple Γ) to a univalent type (of type U):

where t.1 and t.2 indexes into the context tuple Γ to retrieve the
schemas of q1 and q2 respectively.
Note the manipulation of the context tuple in the denotation
of WHERE: for each tuple t, we first evaluate t against the query
before WHERE, using the context tuple g. After that, we evaluate the
predicate b by first constructing a new context tuple as discussed
(namely, by concatenating Γ and σ, the schema of q), passing it the
combined tuple (g, t). The combination is needed as t has schema
σ while the predicate b is evaluated under the schema node Γ σ,

JΓ ` bK : Tuple Γ → U

More specifically, the return type U must be a squash type [46, Ch.
3.3]. A squash type can only be a type of 1 element, namely 1, and
a type of 0 element, namely 0. HoTT SQL program with the form
q WHERE b is denoted to the Cartesian product between a univalent
type and a mere proposition.
As an example, suppose a particular tuple t has multiplicity 3 in
query q, i.e., q t = JRKt = 3, where 3 is a univalent type. Since
7

2016/8/9

To see why this definition satisfies the key constraint, note that
k is a key in R if and only if R equals to its self-join on k after
converting the result into a set using DISTINCT. Intuitively, if k is
a key, then self-join of R on k will keep all the tuples of R with
each tuple’s multiplicity unchanged. Conversely, if R satisfies the
self-join criteria, then attribute k holds unique values in R and is
hence a key.

predicates are denoted to propositions, applying the tuple to the
predicate returns either 1 or 0, and the overall result of the query
for tuple t is then either 3 × 0 = 0, or 3 × 1 = 1, i.e., a squash
type.
Expressions and Projections A value expression e is denoted to
a function from a tuple (of type Tuple Γ) to its data type, such as
int and bool (Jτ K):

Functional Dependencies Keys are used in defining functional
dependencies and indexes. A functional dependency constraint
from attribute a to b requires that for any two tuples t1 and t2
in R, (t1 .a = t2 .a) → (t1 .b = t2 .b) In HoTT SQL, two projections a and b forms a functional dependency in relation R if the
following holds:

JΓ ` e : τ K : Tuple Γ → Jτ K

A projection p from Γ to Γ0 is denoted to a function from a tuple of
type Tuple Γ to a tuple of type Tuple Γ0 .
Jp : Γ ⇒ Γ0 K : Tuple Γ → Tuple Γ0

Projections are recursively defined. A projection can be composed
by two projections using “.”. The composition of two projection,
“p1 . p2 ”, where p1 is a projection from Γ to Γ0 and p2 is a
projection from Γ0 to Γ00 , is denoted to a function from a tuple
of type Tuple Γ to a tuple of type Tuple Γ00 as follows:

fd (a b) (R) :=
key Left.* Jempty ` DISTINCT SELECT a, b
FROM R : node (leaf τa ) (leaf τb )K

λ g. Jp2 : Γ0 ⇒ Γ00 K (Jp1 : Γ ⇒ Γ0 K g)

If a and b forms a functional dependency, then a should be a key
in the relation the results from projecting a and b from R followed
by de-duplication. The converse argument follows similarly.

We apply the denotation of p1 , which is a function of type
Tuple Γ → Tuple Γ0 , to the argument of composed projection
g, then apply the denotation of p2 to the result of application. A
projection can also be combined by two projections using “,”. The
combining of two projection, p1 , p2 , is denoted to:

Index An index on an attribute a is a data structure that speeds
up the retrieval of tuples with a given value of a [18, Ch. 8].
To reason about rewrite rules that use indexes, we follow the
idea that index can be treated as a logical relation rather than physical data structure from Tsatalos et al [49]. Since defining index as
an relation requires a unique identifier of each tuple (analogous to
a pointer to each tuple in the physical implementation of an index
in database systems), we define index as a HoTT SQL query that
projects on the a key of the relation and the index attribute. For example, if k is a key of relation R, an index I of R on attribute a can
be defined as:

λ g. (Jp1 : Γ ⇒ Γ0 K g, Jp2 : Γ ⇒ Γ1 K g)

where we apply the denotation of p1 and the denotation of p2 to the
argument of combined projection (g) separately, and combine their
results using the constructor of a pair.
4.2

Denoting Derived HoTTSQL Constructs

HoTT SQL supports additional SQL features including group by,
integrity constraints, and index. All such features are commonly
utilized in query optimization.

index(a, R) := SELECT k, a FROM R
In Section 5.1.4, we show example rewrite rules that utilize indexes
that are commonly used in query optimizers.

Grouping Grouping is a widely-used relational operator that
projects rows with a common value into separate groups, and applies an aggregation function (e.g., average) to each group. In SQL,
this is supported via the GROUP BY operator that takes in the attribute names to form groups. HoTT SQL supports grouping by
de-sugaring GROUP BY using correlated subqueries that returns a
single attribute relation, and applying aggregation function to the
resulting relation [6]. Below is an example of such rewrite expressed using SQL:

5.

D OP C ERT: A Verified System for Proving
Rewrite Rules

To demonstrate the effectiveness of HoTT SQL, we implement
D OP C ERT, a system written in Coq for checking the equivalence
of SQL rewrite rules. D OP C ERT consists of four parts, 1) the denotational semantics of HoTT SQL, 2) a library consisting of lemmas and tactics that can be used as building blocks for constructing
proofs of arbitrary rewrite rules, 3) a fully automated decision procedure for the equivalence of rewrite rules consisting only of conjunctive queries, and 4) a number of proofs of existing rewrite rules
from the database literature and real world systems.
D OP C ERT relies on the Homotopy Type Theory Coq library [24].
Its trusted code base contains 296 lines of specification of HoTT SQL.
Its verified part contains 405 lines of library code (including the decision procedure for conjunctive queries), and 1094 lines of code
that prove well known SQL rewrite rules.
In the following sections, we first show various rewrite rules and
the lemmas they use from the D OP C ERT library, and then explain
our automated decision procedure.

SELECT k, SUM(g) FROM R GROUP BY k
rewrites to ⇓
SELECT DISTINCT k, SUM( SELECT g FROM R
WHERE R.k = R1 .k)
FROM R AS R1
We will illustrate using grouping in rewrite rules in Sec. 5.1.2.
Integrity Constraints Integrity constraints are used in real-world
database systems and facilitate various semantics-based query optimizations [15]. HoTT SQL supports two important integrity constraints: keys and functional dependency, through syntactic rewrite.
A key constraint requires an attribute to have unique values
among all tuples in a relation. In HoTT SQL, a projection k is a
key to the relation R if the following holds:

5.1

Proving Rewrite Rules in D OP C ERT by Examples

key (k) (R) :=
Jempty ` SELECT * FROM R : σK =
Jempty ` SELECT Left.* FROM R, R
WHERE (P2E Right.Left.k) = (P2E Right.Right.k) : σK

We proved 23 rewrite rules from both the database literature and
real world optimizers using HoTT SQL. Figure 8 shows the number
of rewrite rules that we proved in each category and the average
lines of code (LOC) required per proof.
The following sections show a sampling of interesting rewrite
rules in these categories. Sec 5.1.1 shows how two basic rewrite

8

2016/8/9

Category
Basic
Aggregation
Subquery
Magic Set
Index
Conjunctive Query
Total

No. of rules
8
1
2
7
3
2
23

Avg. LOC (proof only)
11.1
50
17
30.3
64
1 (automatic)
25.2

Together with the fact that t1 = (t1 .1, t1 .2), the rewrite rule’s
right hand side becomes:
λ g t.

t0

Lemma 5.2. Let A and B inhabit U, and have P : A × B → U,
then we have:
X
P x=
P x0 × (x0 = x)

rules are proved. Sec 5.1.2 shows how to prove a rewrite rule
involving aggregation. Sec 5.1.3 shows how to prove the magic set
rewrite rules. Sec 5.1.4 shows how to state a rewrite rule involving
indexes.

x0

After applying Lemma 5.2, the right hand side becomes the
following, and we can finish the proof by applying commutativity
of ×:
λ g t. JSK g t.2 × JRK g t.1

Basic Rewrite Rules

Basic rewrites are simple rewrite rules that are fundamental building blocks of the rewriting system. These rewrites are also very effective in terms of reducing query execution time. We demonstrate
how to prove the correctness of basic rewrite rules in D OP C ERT using two examples: selection push down and commutativity of joins.

5.1.2

JΓ ` SELECT * FROM R WHERE p1 AND p2 : σK ≡
JΓ ` SELECT * FROM
(SELECT * FROM R WHERE p1 ) WHERE p2 : σK

JΓ ` SELECT * FROM (SELECT k, SUM(b) FROM R GROUP BY k)
WHERE (P2E k) = l : σK ≡
JΓ ` SELECT k, SUM(b) FROM R WHERE (P2E k) = l GROUP BY k : σK

This will be denoted to:
λ g t. Jp1 K(g, t) × Jp2 K (g, t) × JRK g t
λ g t. Jp2 K (g, t) × (Jp1 K (g, t) × JRK g t)

As shown in Sec. 4.2, we use a correlated subquery and a unary
aggregate function (which takes a HoTT SQL query as its input) to
represent aggregation on group by SQL queries. After de-sugaring,
the group by query becomes SELECT DISTINCT . . .. The rule will
thus be denoted to:

≡

The proof proceeds by functional extensionality 4 and the associativity and commutativity of ×.
Commutativity of Joins Commutativity of joins allows an optimizer to rearrange the order of joins in order to get the join order
with best performance. This is one of the most fundamental rewrite
rules that almost every optimizer uses. We formulate the commutativity of joins in HoTT SQL as follows:
JΓ ` SELECT * FROM R, S : node σR σS K ≡
JΓ ` SELECT Right.Right.*, Right.Left.* FROM S, R : node σR σS K

Note that the select clause flips the tuples from S and R, such
that the order of the tuples matches the original query. This will be
denoted to:
λ g t. JRK
P g t.1 × JSK g t.2 ≡
λ g t.
t1 JSK g t1 .1 × JRK g t1 .2 × ((t1 .2, t1 .1) = t)

P
λ g t. (t.1 = JlK) × k t1 JRK
P t1 × (t.1 = JkK t1 )×
(t.2 = JSUMK (λ t0 .
t2 (JkK t1 = JkK t2 )×
JRK t2 × (JbK t1 = t0 ))k
≡
P
λ g t. k t1 (JkK t1 = JlK)P
× JRK t1 × (t.1 = JkK t1 )×
(t.2 = JSUMK (λ t0 .
t2 (JkK t1 = JkK t2 ) × (JkK t2 = JlK)×
JRK t2 × (JbK t1 = t0 ))k

The proof proceeds by functional extensionality, after which
both sides become squash types. The proof then uses the fundamental lemma about squash types, where for all squash types A
and B, (A ↔ B) ⇒ (A = B). It thus suffices to prove by
cases the bi-implication (↔) of both sides. In both cases, instantiate t1 with t1 (t1 is the witness of the Σ hypothesis). It follows
that t.1 = JlK = JkK t1 , and thus that JkK t2 = JlK inside SUM.
5.1.3

The proof uses Lemma 5.1 provided by the D OP C ERT library.

Magic Set Rewrite Rules

Magic set rewrites are well known rewrite rules that were originally
used in the recursive query processing in deductive databases [2,
41]. It was then used for rewriting complex decision support queries
and has been implemented in commercial systems such as IBM’s
DB2 database [36, 44]. Below is an example of a complex magic
set rewrite from [44].
Original Query:

Lemma 5.1. Let A inhabit U, and have P : A → U be a type
family, then we have:
X
X
P x=
P (x.2, x.1)
4 Function

Aggregation and Group By Rewrite Rules

Aggregation and Group By are widely used in analytic queries [9].
The standard data analytic benchmark TPC-H [48] has 16 queries
with group by and 21 queries with aggregation out of a total of 22
queries. Following is an example rewrite rule for aggregate queries.
The query on the left-hand side groups the relation R by the column
k, sums all values in the b column for each resulting partition, and
then removes all results except the partition whose column k is
equal to the constant l. This can be rewritten to the faster query
that first removes all tuples from R whose column k 6= l, and then
computes the sum.

Selection Push Down Selection push down moves a selection
(filter) directly after the scan of the input table to dramatically
reduce the amount of data in the execution pipeline as early as
possible. It is known as one of most powerful rules in database
optimizers [18]. We formulate selection push down as the following
rewrite rule in HoTT SQL:

x:A×B

JSK g t0 .2 × JRK g t0 .1 × (t0 = t)

The proof then uses Lemma 5.2 provided by the D OP C ERT
library.

Figure 8. Rewrite rules proved

5.1.1

X

x:B×A

extensionality is implied by the Univalence Axiom.

9

2016/8/9

Pushing θ-semijoin through join The second rule in magic set
rewrites is the rule for pushing θ-semijoin through join, represented
in semijoin algebra as:

CREATE VIEW DepAvgSal AS
(SELECT E.did, AVG(E.sal) AS avgsal FROM Emp E
GROUP BY E.did);
SELECT E.eid, E.sal FROM Emp E, Dept D, DepAvgSal V
WHERE E.did = D.did AND E.did = V.did AND E.age < 30
AND D.budget > 100000 AND E.sal > V.avgsal

(R1 ./θ1 R2 ) nθ2 R3 ≡ (R1 ./θ1 R20 ) nθ2 R3
where R20 = E2 nθ1 ∧θ2 (R1 ./ R3 ). This rule can be written in
HoTT SQL as below:

Rewritten Query:

λ g t. JΓ ` (SELECT * FROM R1 , R2 WHERE θ1 )
SEMIJOIN R3 ON θ2 : node σ1 σ2 K ≡
λ g t. JΓ ` (SELECT *
FROM R1 , (R2 SEMIJOIN (FROM R1 , R3 ) ON θ1 AND θ2 )
WHERE θ1 ) SEMIJOIN R3 ON θ2 : node σ1 σ2 K

CREATE VIEW P artialResult AS
(SELECT E.eid, E.sal, E.did FROM Emp E, Dept D
WHERE E.did = D.did AND E.age < 30 AND
D.budget > 100000);
CREATE VIEW F ilter AS
(SELECT DISTINCT P.did FROM P artialResult P );
CREATE VIEW LimitedDepAvgSal AS
(SELECT F.did, AVG(E.sal) AS avgsal
FROM F ilter F , Emp E
WHERE E.did = F.did
GROUP BY F.did);
SELECT P.eid, P.sal
FROM P artialResult P , LimitedDepAvgSal V
WHERE P.did = V.did AND P.sal > V.avgsal

The rule is denoted to:

This query aims to find each young employee in a big department (D.budget > 100000) whose salary is higher then the average salary in her department. Magic set rewrites use the fact that
only the average salary of departments that are big and have young
employees need to be computed. As described in [44], all magic
set rewrites can be composed from just three basic rewrite rules on
semijoins, namely introduction of θ-semijoin, pushing θ-semijoin
through join, and pushing θ-semijoin through aggregation.
Following, we show how to state all three rewrite rules using D OP C ERT, and show how to prove two. We firstly define θsemijoin as a syntactic rewrite in HoTT SQL:

We can prove this rule by using a similar approach to the one
used to prove introduction of θ-semijoin: rewriting the right hand
side using Lemma 5.3. and then instantiating t1 with (t.1, t1 ) (t1 is
the witness of the Σ hypothesis).
Pushing θ-semijoin through aggregation The final rule is pushing θ-semijoin through aggregation:
ḡ Ff¯(R1 )

nc1 =c2 R2 ≡ḡ Ff¯(R1 nc1 =c2 R2 )
where ḡ Ff¯ is a grouping/aggregation operator (ḡ Ff¯ was firstly
defined in [44]), and ḡ denotes the group by attributes and f¯ denotes
the aggregation function. In this rule, one extra condition is that c1
is from the attributes in ḡ and c2 is from the attributes of R2 . This
rule can be written in HoTT SQL as below:

A SEMIJOIN B ON θ ,
SELECT * FROM A WHERE EXISTS (SELECT * FROM B WHERE θ)

Introduction of θ-semijoin This rules shows how to introduce
semijoin from join and selection. Using semijoin algebra notation,
this rewrite can be expressed as follows:

JΓ ` (SELECT c1 , COUNT(a) FROM R1 GROUP BY c1 )
SEMIJOIN R2 ON c1 = c2 : σK ≡
JΓ ` SELECT c1 , COUNT(a)
FROM (R1 SEMIJOIN R2 ON c1 = c2 ) GROUP BY c1 : σK

R1 ./θ R2 ≡ R1 ./θ (R2 nθ R1 )
Using HoTT SQL, the rewrite can be expressed as follows:

We omit the proof here for brevity.
5.1.4

JΓ ` SELECT * FROM R2 , R1 WHERE θ : σK
≡
JΓ ` SELECT * FROM (R2 SEMIJOIN R1 ON θ), R1 WHERE θ : σK

Index Rewrite Rules

As introduced in Section 4.2, we define an index as a HoTT SQL
query that projects on the indexed attribute and the primary key of
a relation. Assuming k is the primary key of relation R, and I is an
index on column a:

which is denoted to:
λ g t. JθK (g, t) × JR2 K g t.1 × JR1 K g t.2
λ g t. JθK (g, t) × JR2 K g t.1 × JR1 K g t.2 ×
P
t1 JθK (g, (t.1, t1 )) × JR1 K g t1

P

t1 Jθ2 K (g, (t, t1 )) × JR3 K g t1 ×
Jθ1 K (g, t) × JR1 K g t.1 × JR2 K g t.2
≡
P
λ g t.
t1 Jθ2 K (g, (t, t1 )) × JR3 K g t1 ×
JθP
1 K (g, t) × JR1 K g t.1 × JR2 K g t.2 ×
k t1 Jθ1 K (g, (t1 .1, t.2)) × Jθ2 K (g, ((t1 .1, t.2), t1 .2))
×JR1 K g t1 .1 × JR3 K g t1 .2k

λ g t.

≡

I := SELECT k, a FROM R
We prove the following common rewrite rule that converts a full
table scan to a lookup on an index and a join:

The proof uses Lemma 5.3 provided by the D OP C ERT library.

JΓ ` SELECT * FROM R WHERE a = l : σK ≡
JΓ ` SELECT * FROM I, R
WHERE a = l AND Right.Left.k = Right.Right.k : σK

Lemma 5.3. ∀P, T : U, where P is either 0 or 1, we have:
(T → P ) ⇒ ((T × P ) = T )
Proof. Intuitively, this can be proven by cases on T . If T is inhabited, then P holds by assumption, and T × 1 = T . If T = 0, then
0 × P = 0.

We omit the proof here for brevity.
5.2

Automated Decision Procedure for Conjunctive Queries

The equivalence of two SQL queries is in general undecidable. FigUsing this lemma, it remains to be shown that JθK (g, t) and
ure 9 shows the complexities of deciding containment and equivaP
JR2 K g t.1 and JR1 K g t.2 imply
t1 JθK (g, (t.1, t1 )) × JR1 K g t1 . lence of subclasses of SQL. The most well-known subclass are conjunctive queries, which are of the form DISTINCT SELECT p FROM
We show this by instantiating t1 with t.2, and then by hypotheses.

10

2016/8/9

Conjunctive Queries
Union of Conjunctive Queries
Conjunctive Query with 6=, ≥, and ≤
First Order (SQL) Queries

Containment (Set)
NP-Complete [8]
NP-Complete [42]
Πp2 -Complete [52]
Undecidable [47]

Containment (Bag)
Open
Undecidable [27]
Undecidable [29]
Undecidable

Equivalence (Set)
NP-Complete [8]
NP-Complete [42]
Πp2 -Complete [52]
Undecidable

Equivalence (Bag)
Graph Isomorphism [10]
Open
Undecidable [29]
Undecidable

Figure 9. Complexities of Query Containment and Equivalence

σ R1

σ R2

P
λ g t. k t1 JR1 K gt1 .1 × JR2 K g t1 .2 ×
(Jc2 K t1 .1 = Jc3 K t1 .2) ×
(Jc
≡
P1 K t1 .1 = t) × k
λ g t. k t1 JR1 K g t1 .1.1 × JR1 K g t1 .1.2 × JR2 K g t1 .2 ×
(Jc1 K t1 .1.1 = Jc1 K t1 .1.2) × (Jc2 K t1 .1.1 = Jc3 K t1 .2) ×
(Jc1 Kt1 .1.1 = t)k

σR2

σ R1

The decision procedure turns this goal into a bi-implication,
which it proves by cases. For the → case, the decision procedure
destructs the available Σ witness into tuple tx from R1 and ty from
R2 and tries all instantiations of t1 using these tuples. The instantiation t1 = ((tx , tx ), ty ) allows the procedure to complete the
proof after rewriting all equalities. For the ← case, the available
tuples are tx from R1 , ty from R1 , and tz from R2 . The instantiation t1 = (tx , tz ) allows the procedure to complete the proof after
rewriting all equalities. This assignment is visualized in Figure 10.

σ R1
Schema of t1 (right)

Schema of t1 (left)

σ R1

which is denoted as:

Schema of t1 (right)

Schema of t1 (left)

σR2

σR2

σ R1

σR1

Figure 10. The mappings found to prove the conjunctive query
example, blue lines show the mapping found to prove left → right,
red lines show the mapping found to prove right → left.

Related Work

6.1

Query Rewriting

Query rewriting based on equivalence rules is an essential part
of modern query optimizers. Rewrite rules are either fired by a
forward chaining rule engine in a Starburst optimizer framework
[25, 40], or are used universally to represent the search space
in Exodus [21] and its successors, including Volcano [22] and
Cascades [20].
Using D OP C ERT, we formally prove a series of rewrite rules
from the database literature. Those rules include basic algebraic
rewrites such as selection push down [50], rewrite rules using
indexes [18], and unnesting aggregates with joins [37]. We are
able to prove one of the most complicated rewrite rules that is also
widely used in practice: magic set rewrites [2, 36, 44]. Magic set
rewrites involve many SQL features such as correlated subqueries,
aggregation and group by. To our best knowledge, its correctness
has not been formally proven before.
D OP C ERT automates proving rewrite rules on decidable fragments of SQL. According to Codd’s theorem [14], relational algebra and relational calculus (formulas of first-order logic on database
instances) are equivalent in expressive power. Thus, the equivalence between two SQL queries is in general undecidable [47].
Extensive research has been done to study the complexity of containment and equivalence of fragments of SQL queries under bag
semantics and set semantics [8, 10, 19, 27, 29, 42, 52]. We list the
results in Figure 9.

q WHERE b, where p is a sequence of arbitrarily many attribute projections, q is the cross product of arbitrarily many input relations,
and b is a conjunct consisting of arbitrarily many equality predicates between attribute projections.
We implement a decision procedure to automatically prove the
equivalence of conjunctive queries in HoTT SQL. After denoting the HoTT SQL query to U NI N OMIAL, the decision procedure
automates steps similar to the proof in Section 5.1.2. First, after applying functional extensionality, both sides become squash
types due to the DISTINCT clause. The procedure then applies
the fundamental lemma about squash types ∀AB, (A ↔ B) ⇒
(A = B). In both cases of the resulting bi-implication, the procedure tries all possible instantiations of the Σ, which is due to the
SELECT clause. This search for the correct instantiation is implemented using Ltac’s built-in backtracking support. The procedure
then rewrites all equalities and tries to discharge the proof by direct
application of hypotheses.
The following is an example of two equivalent conjunctive SQL
queries that we can solve using our decision procedure:
SELECT DISTINCT x.c1 FROM R1 AS x, R2 AS y
WHERE x.c2 = y.c3
SELECT DISTINCT x.c1 FROM R1 AS x, R1 AS y, R2 AS z
WHERE x.c1 = y.c1 AND x.c2 = z.c3

6.

6.2

≡

SQL Semantics

SQL is the de-facto language for relational database systems. Although the SQL language is an ANSI/ISO standard [28], it is
loosely described in English and leads to conflicting interpretations
[16]. Previous related formalizations of various fragments of SQL
include relational algebra [1], comprehension syntax [6], and recursive and non-recursive Datalog [10]. These formalisms are not
suited for rigorous reasoning about the correctness of real world
rewrite rules since they mostly focus exclusively on set semantics.
In addition, in order to express rewrite rules in these formalism,
non-trivial transformation from SQL are required.

The same queries can be expressed in HoTT SQL as follows,
where the schema of Ri is σRi :
JΓ ` DISTINCT SELECT Right.Left.c1 FROM R1 , R2
WHERE Right.Left.c2 = Right.Right.c3 : σK ≡
JΓ ` DISTINCT SELECT Right.Left.Left.c1
FROM (FROM R1 , R1 ), R2
WHERE Right.Left.Left.c1 = Right.Left.Right.c1 AND
Right.Left.Left.c2 = Right.Right.c3 : σK

11

2016/8/9

A direct implementation in HoTT SQL would basically have to
follow the same definition of left outer joins.
Finite v.s. Infinite Semantics Recall that our semantics extends the standard bag semantics of SQL in two ways: we allow
a relation to have infinitely many distinct elements, and we allow each element to have an infinite multiplicity. To the best of
our knowledge, our system is the first that interprets SQL over
infinite relations. This has two consequences. First, our system
cannot check the equivalence of two SQL expressions that return
the same results on all finite relations, but differ on some infinite relations. It is well-known that there exists First Order sentences, called infinity axioms, that do not admit any finite model,
but admit infinite models. For example [5, pp.307] the sentence
ϕ ≡ ∀x∃y∀z(¬R(x, x)∧R(x, y)∧(R(y, z) → R(x, z))) is an infinity axiom. It is possible to write a SQL query that checks ϕ, then
returns the empty set if ϕ is false, or returns a set consisting of a single value (say, 1) if ϕ is true: call this query Q1 . Call Q2 the query
SELECT DISTINCT 1 FROM R WHERE 2=3. Then Q1 = Q2
over all finite relations, but Q1 6= Q2 not over infinite relations.
Thus, one possible disadvantage of our semantics is that we cannot
prove equivalence of queries that encode infinity axioms. However,
none of the optimization rules that we found in the literature, and
discussed in this paper, encode an infinity axiom. Hence we argue
that, for practical purposes, extending the semantics to infinite relations is a small price to pay for the added simplicity of the equivalence proofs. Second, by generalizing SQL queries to both finite
and infinite relations we make our system theoretically complete: if
two queries are equivalent then, by Gödel’s completeness theorem,
there exists a proof of their equivalence. Finding the proof is undecidable (it is recursively enumerable, r.e.): our system does not
search for the proof, instead the user has to find it, and our system
will verify it. Contrast this with a system whose semantics is based
on finite relations: such a system cannot have a complete proof system for SQL query equivalence. Indeed, if such a complete proof
system existed, then SQL query equivalence would be r.e. (since
we can enumerate all proofs and search for a proof of Q1 = Q2 ),
and therefore equivalence would be decidable (since it is also cor.e., because we can enumerate all finite relations, searching for an
input s.t. Q1 6= Q2 ). However, by Trakthenbrot’s, query equivalence is undecidable. Recall that Trakthenbrot’s theorem [34, 47]
states that the problem given an FO sentence ϕ, check if ϕ has a
finite model is undecidable. We can reduce this problem to query
equivalence by defining Q1 to be a query that checks checks ϕ and
returns the empty set if ϕ is false, or returns some non-empty set if
ϕ is true, and defining Q2 to be the query that always returns the
empty set (as above), then checking Q1 ≡ Q2 ). Thus, by extending
our semantics to infinite relations we guarantee that, whenever two
queries are equivalent, there exists a proof of their equivalence.

Previous SQL formalizations in proof systems include [4, 35,
53, 54]. In [53, 54], SQL semantics are encoded in the Z3 SMT
solver for test generation. In [35], an end to end verified prototype
database system is implemented in Coq. In [4], a relational data
model and relational algebra are implemented in Coq. Compared
with [4, 35], HoTT SQL covers all important SQL feature such as
bags, aggregation, group by, indexes, and correlated subqueries. As
a result, we are able to express a wide range of rewrite rules. Unlike
[35], we did not build an end to end formally verified database
system.
In HoTT SQL, SQL features like aggregation on group by and
indexes are supported through syntactic rewrites. Rewriting aggregation on group by using aggregation on relations and correlated
subqueries is based on [6]. We use logical relation to represent indexes in HoTT SQL. This was firstly proposed by Tastalos et al
[49].
6.3

Related Formal Semantics in Proof Systems

In the past decades, a number of formal semantics in different application domains were developed using proof systems for software verification. The CompCert compiler [32] specifies the semantics of a subset of C in Coq and provides machine checkable
proofs of the correctness of compilation. HALO denotes Haskell
to first-order logic for static verification of contracts [55]. Bagpipe
[56] developed formal semantics for the Border Gateway Protocol
(BGP) to check the correctness of BGP configurations. SEL4 [31]
formally specifies the functional correctness of an OS kernel in Isabelle/HOL and developed a verified OS kernel. FSCQ [11] builds
a crash safe file system using an encoding of crash Hoare logic in
Coq. With formal semantics in proof systems, there are more verified system developed such as Verdi [57], Verve [58], Bedrock [12]
and Ironclad [26].

7.

Discussion

Limitations Our system does currently not support three SQL
features: NULL’s with their associated three-valued-logic, outer
joins, and windows functions. However, all can be expressed in
HoTT SQL, at the cost of some added complexity, as we explain
now.
When any argument to an expression is NULL, then the expression’s output is NULL; this feature can easily be supported by modifying the external operators. When an argument of a comparison
predicate is NULL, then the resulting predicate has value unknown,
and SQL uses three valued logic to compute predicates: it defines
0 = false, 1/2 = unknown, 1 = true, and the logical operators
x and y = min(x, y), x or y = max(x, y), not(x) = 1 − x;
a select-from-where query returns all tuples for which the wherepredicate evaluates to true (i.e. not false or unknown). As a consequence, the law of excluded middle fails, for example the query:

8.

SELECT * FROM R WHERE a = 5 or a 6= 5

Conclusion

We have described D OP C ERT, a system for proving equivalence of
SQL rewrite rules. In support of D OP C ERT, we defined a formal
language HoTT SQL, following closely SQL’s syntax. Our semantics extends that of SQL from finite relations to infinite relations,
and uses univalent types from Homotopy Type Theory to represent and prove equality of cardinal numbers (finite and infinite). We
have demonstrated the power and flexibility of D OP C ERT by proving the correctness of several powerful optimization rules found in
the database literature.

is not equivalent to SELECT * FROM R. This, too, could be currently
expressed HoTT SQL by encoding the predicates as external functions that implement the 3-valued logic. However, by doing so one
hides from the rewrite rules the equality predicate, which plays a
key role in joins. In future versions, we plan to offer native support for NULL’s, to simplify the task of proving rewrite rules over
relations with NULLs.
Both outer joins and windows functions are directly expressible in HoTT SQL. For example, a left outer join of two relations
R(a, b), S(b, c) can be expressed by first joining R and S on b, and
union-ing the result with
SELECT R.∗, NULL FROM S EXCEPT
SELECT R.∗, NULL FROM S WHERE R.b = S.b
12

2016/8/9

References

[26] C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang,
and B. Zill. Ironclad apps: End-to-end security via automated fullsystem verification. In OSDI, pages 165–181. USENIX Association,
2014.
[27] Y. E. Ioannidis and R. Ramakrishnan. Containment of conjunctive
queries: Beyond relations as sets. ACM Trans. Database Syst., 20(3):
288–324, 1995.
[28] ISO/IEC. Iso/iec 9075-1:2011. https://www.iso.org/obp/ui/
#iso:std:iso-iec:9075:-1:ed-4:v1:en. Online; accessed 9May-2016.
[29] T. S. Jayram, P. G. Kolaitis, and E. Vee. The containment problem for
REAL conjunctive queries with inequalities. In PODS, pages 80–89.
ACM, 2006.
[30] M. A. Khamis, H. Q. Ngo, and A. Rudra. FAQ: questions asked
frequently. In PODS, pages 13–28, 2016.
[31] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin,
D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell,
H. Tuch, and S. Winwood. sel4: formal verification of an OS kernel.
In SOSP, pages 207–220. ACM, 2009.
[32] X. Leroy. Formal verification of a realistic compiler. Commun. ACM,
52(7):107–115, 2009.
[33] A. Y. Levy, I. S. Mumick, and Y. Sagiv. Query optimization by
predicate move-around. In VLDB, pages 96–107. Morgan Kaufmann,
1994.
[34] L. Libkin. Elements of Finite Model Theory. Texts in Theoretical
Computer Science. An EATCS Series. Springer.
[35] J. G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Toward
a verified relational database management system. In POPL, pages
237–248, 2010.
[36] I. S. Mumick, S. J. Finkelstein, H. Pirahesh, and R. Ramakrishnan.
Magic is relevant. In SIGMOD Conference, pages 247–258, 1990.
[37] M. Muralikrishna. Improved unnesting algorithms for join aggregate
SQL queries. In VLDB, pages 91–102. Morgan Kaufmann, 1992.
[38] M. Negri, G. Pelagatti, and L. Sbattella. Formal semantics of SQL
queries. ACM Trans. Database Syst., 16(3):513–534, 1991.
[39] G. Nelson and D. C. Oppen. Fast decision procedures based on
congruence closure. J. ACM, 27(2):356–364, 1980.
[40] H. Pirahesh, J. M. Hellerstein, and W. Hasan. Extensible/rule based
query rewrite optimization in starburst. In SIGMOD Conference,
pages 39–48. ACM Press, 1992.
[41] J. Rohmer, R. Lescoeur, and J. Kerisit. The alexander method - A technique for the processing of recursive axioms in deductive databases.
New Generation Comput., 4(3):273–285, 1986.
[42] Y. Sagiv and M. Yannakakis. Equivalences among relational expressions with the union and difference operators. J. ACM, 27(4):633–655,
1980.
[43] D. Schmitt. Bug #5673: Optimizer creates strange execution plan leading to wrong results. https://www.postgresql.org/message-id/
201009231503.o8NF3Blt059661@wwwmaster.postgresql.org.
Online; accessed 1-July-2016.
[44] P. Seshadri, J. M. Hellerstein, H. Pirahesh, T. Y. C. Leung, R. Ramakrishnan, D. Srivastava, P. J. Stuckey, and S. Sudarshan. Cost-based
optimization for magic: Algebra and implementation. In SIGMOD
Conference, pages 435–446, 1996.
[45] M. Sulik. Bug #70038: Wrong select count distinct with a field
included in two-column unique key. http://bugs.mysql.com/bug.
php?id=70038. Online; accessed 1-July-2016.
[46] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.
org/book, Institute for Advanced Study, 2013.
[47] B. A. Trakhtenbrot. Impossibility of an algorithm for the decision
problem in finite classes. Dok. Akad. Nauk USSR, 70(1):569–572,
1950.
[48] Transaction Processing Performance Council (TPC). Tpc benchmark
h revision 2.17.1. http://www.tpc.org/tpc_documents_current_
versions/pdf/tpc-h_v2.17.1.pdf.

[1] S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases.
Addison-Wesley, 1995. URL http://webdam.inria.fr/Alice/.
[2] F. Bancilhon, D. Maier, Y. Sagiv, and J. D. Ullman. Magic sets and
other strange ways to implement logic programs. In PODS, pages 1–
15, 1986.
[3] B. Barras, B. Grégoire, A. Mahboubi, and L. Théry. Coq reference
manual chapter 25: The ring and field tactic families. https://coq.
inria.fr/refman/Reference-Manual028.html.
[4] V. Benzaken, E. Contejean, and S. Dumbrava. A coq formalization of
the relational data model. In ESOP, pages 189–208, 2014.
[5] E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.
[6] P. Buneman, L. Libkin, D. Suciu, V. Tannen, and L. Wong. Comprehension syntax. SIGMOD Record, 23(1):87–96, 1994.
[7] P. Buneman, S. A. Naqvi, V. Tannen, and L. Wong. Principles of programming with complex objects and collection types. Theor. Comput.
Sci., 149(1):3–48, 1995.
[8] A. K. Chandra and P. M. Merlin. Optimal implementation of conjunctive queries in relational data bases. In STOC, pages 77–90. ACM,
1977.
[9] S. Chaudhuri and U. Dayal. An overview of data warehousing and
OLAP technology. SIGMOD Record, 26(1):65–74, 1997.
[10] S. Chaudhuri and M. Y. Vardi. On the complexity of equivalence
between recursive and nonrecursive datalog programs. In PODS,
pages 107–116. ACM Press, 1994.
[11] H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek, and
N. Zeldovich. Using crash hoare logic for certifying the FSCQ file
system. In SOSP, pages 18–37, 2015.
[12] A. Chlipala. The bedrock structured programming system: combining
generative metaprogramming and hoare logic in an extensible program
verifier. In ICFP, pages 391–402. ACM, 2013.
[13] E. F. Codd. A relational model of data for large shared data banks.
Commun. ACM, 13(6):377–387, 1970.
[14] E. F. Codd. Relational completeness of data base sublanguages. In:
R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM
Research Report RJ 987, San Jose, California, 1972.
[15] S. Dar, M. J. Franklin, B. T. Jónsson, D. Srivastava, and M. Tan.
Semantic data caching and replacement. In VLDB, pages 330–341.
Morgan Kaufmann, 1996.
[16] C. J. Date. A Guide to the SQL Standard, Second Edition. AddisonWesley, 1989. ISBN 978-0-201-50209-1.
[17] R. A. Ganski and H. K. T. Wong. Optimization of nested SQL queries
revisited. In SIGMOD Conference, pages 23–33. ACM Press, 1987.
[18] H. Garcia-Molina, J. D. Ullman, and J. Widom. Database systems the complete book (2. ed.). Pearson Education, 2009. ISBN 978-0-13187325-4.
[19] G. Geck, B. Ketsman, F. Neven, and T. Schwentick. Parallelcorrectness and containment for conjunctive queries with union and
negation. In ICDT, volume 48 of LIPIcs, pages 9:1–9:17. Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
[20] G. Graefe. The cascades framework for query optimization. IEEE
Data Eng. Bull., 18(3):19–29, 1995.
[21] G. Graefe and D. J. DeWitt. The EXODUS optimizer generator. In
SIGMOD Conference, pages 160–172. ACM Press, 1987.
[22] G. Graefe and W. J. McKenna. The volcano optimizer generator:
Extensibility and efficient search. In ICDE, pages 209–218. IEEE
Computer Society, 1993.
[23] T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings.
In PODS, pages 31–40, 2007.
[24] J. Gross, M. Shulman, A. Bauer, P. L. Lumsdaine, A. Mahboubi, and
B. Spitters. The hott libary in coq. https://github.com/HoTT/HoTT.
[25] L. M. Haas, J. C. Freytag, G. M. Lohman, and H. Pirahesh. Extensible
query processing in starburst. In SIGMOD Conference, pages 377–
388. ACM Press, 1989.

13

2016/8/9

[49] O. G. Tsatalos, M. H. Solomon, and Y. E. Ioannidis. The GMAP: A
versatile tool for physical data independence. In VLDB, pages 367–
378. Morgan Kaufmann, 1994.
[50] J. D. Ullman. Principles of Database and Knowledge-Base Systems,
Volume II. Computer Science Press, 1989.
[51] J. D. Ullman. Information integration using logical views. In ICDT,
volume 1186 of Lecture Notes in Computer Science, pages 19–40.
Springer, 1997.
[52] R. van der Meyden. The complexity of querying indefinite data about
linearly ordered domains. In PODS, pages 331–345, 1992.
[53] M. Veanes, P. Grigorenko, P. de Halleux, and N. Tillmann. Symbolic
query exploration. In ICFEM, pages 49–68, 2009.
[54] M. Veanes, N. Tillmann, and J. de Halleux. Qex: Symbolic SQL
query explorer. In LPAR (Dakar), volume 6355 of Lecture Notes in
Computer Science, pages 425–446. Springer, 2010.
[55] D. Vytiniotis, S. L. P. Jones, K. Claessen, and D. Rosén. HALO:
haskell to logic through denotational semantics. In POPL, pages 431–
442, 2013.
[56] K. Weitz, D. Woos, E. Torlak, M. D. Ernst, A. Krishnamurthy, and
Z. Tatlock. Bagpipe: Verified BGP configuration checking. Technical
Report UW-CSE-16-01-01, University of Washington Department of
Computer Science and Engineering, Seattle, WA, USA, Jan. 2016.
[57] J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D.
Ernst, and T. E. Anderson. Verdi: a framework for implementing
and formally verifying distributed systems. In PLDI, pages 357–368.
ACM, 2015.
[58] J. Yang and C. Hawblitzel. Safe to the last instruction: automated
verification of a type-safe operating system. In PLDI, pages 99–110.
ACM, 2010.

14

2016/8/9

