Email Gateway (Sep 29 2022 at 08:33): Email Gateway (Sep 29 2022 at 08:33):From: Tobias Nipkow <nipkow@in.tum.de>
Making Arbitrary Relational Calculus Queries Safe-Range
Martin Raszyk and Dmitriy Traytel
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.)
https://www.isa-afp.org/entries/Safe_Range_RC.html
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC