4
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries

      Preprint

      , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Deciding the equivalence of SQL queries is a fundamental problem in data management. As prior work has mainly focused on studying the theoretical limitations of the problem, very few implementations for checking such equivalences exist. In this paper, we present a new formalism and implementation for reasoning about the equivalences of SQL queries. Our formalism, U-semiring, extends SQL's semiring semantics with unbounded summation and duplicate elimination. U-semiring is defined using only very few axioms and can thus be easily implemented using proof assistants such as Coq for automated query reasoning. Yet, they are sufficient enough to enable us reason about sophisticated SQL queries that are evaluated over bags and sets, along with various integrity constraints. To evaluate the effectiveness of U-semiring, we have used it to formally verify 39 query rewrite rules from both classical data management research papers and real-world SQL engines, where many of them have never been proven correct before.

          Related collections

          Most cited references 12

          • Record: found
          • Abstract: not found
          • Conference Proceedings: not found

          Optimal implementation of conjunctive queries in relational data bases

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Fast Decision Procedures Based on Congruence Closure

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Equivalences Among Relational Expressions with the Union and Difference Operators

                Bookmark

                Author and article information

                Journal
                06 February 2018
                Article
                1802.02229

                http://creativecommons.org/licenses/by-nc-sa/4.0/

                Custom metadata
                cs.DB cs.PL

                Comments

                Comment on this article