Abstract
The relational calculus (RC), i.e., first-order logic with equality
but without function symbols, is a concise, declarative database query
language. In contrast to relational algebra or SQL, which are the
traditional query languages of choice in the database community, RC
queries can evaluate to an infinite relation. Moreover, even in cases
where the evaluation result of an RC query would be finite it is not
clear how to efficiently compute it. Safe-range RC is an interesting
syntactic subclass of RC, because all safe-range queries evaluate to a
finite result and it is well-known
how to evaluate such queries by translating them to relational
algebra. We formalize and prove correct our
recent translation of an arbitrary RC query into a pair of
safe-range queries. Assuming an infinite domain, the two queries have
the following meaning: The first is closed and characterizes the
original query's relative safety, i.e., whether given a fixed
database (interpretation of atomic predicates with finite relations),
the original query evaluates to a finite relation. The second
safe-range query is equivalent to the original query, if the latter is
relatively safe. The formalization uses the Refinement Framework to
go from the non-deterministic algorithm described in the paper to a
deterministic, executable query translation. Our executable query
translation is a first step towards a verified tool that efficiently
evaluates arbitrary RC queries. This very problem is also solved by
the AFP entry Eval_FO
with a theoretically incomparable but practically worse time
complexity. (The latter is demonstrated by our
empirical evaluation.)