Formal correctness proof of a mapping from a software specification language to the relational algebra

Abstract

This thesis explores the connection between predicate logic and relational algebra, two foundational pillars of database theory.

We introduce a mapping from logical formulae to relational algebra and prove the semantic equivalence between the two domains. This correspondence creates opportunities for query optimization and enables the use of database queries via a declarative approach, arguably more readable and less error-prone.

The logical formulae introduced are part of our language, which is essentially the predicate logic but without function symbols. On the other hand, the relational algebra formalized in this project is the standard one.

Additional features are also presented in this work. In particular, we extend our language, we formalize a type system for our relations and language – and the correspondence proven between these two domains can also be established under our type system.

While still not widely used, theorem provers are getting increasingly important in computer science where software needs to be reliable. Hence, all results and proofs from this project are rigorously formalized using the Isabelle theorem prover, ensuring that our proofs are free from human error.