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

### License

BSD License

### Topics

- Computer science/Data management systems
- Logic/General logic/Classical first-order logic

### Session Safe_Range_RC

- Preliminaries
- Relational_Calculus
- Restrict_Bounds
- Restrict_Bounds_Impl
- Restrict_Frees
- Restrict_Frees_Impl
- Examples
- Results

### Depends on

- Collections Framework
- Deriving class instances for datatypes
- List Index

## Cite

×

Safe_Range_RC-AFP

    @article{Safe_Range_RC-AFP,
      author  = {Martin Raszyk and Dmitriy Traytel},
      title   = {Making Arbitrary Relational Calculus Queries Safe-Range},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Safe_Range_RC.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Sep 29, 2022 : Isabelle2021-1