Making Arbitrary Relational Calculus Queries Safe-Range

Martin Raszyk 📧 and Dmitriy Traytel 🌐

September 28, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.)


BSD License


Session Safe_Range_RC