{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T17:44:58Z","timestamp":1785606298694,"version":"3.56.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"11","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:p>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 Lean 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 68 equivalent queries and rewrite rules from both classical data management research papers and real-world SQL engines, where many of them have never been proven correct before.<\/jats:p>","DOI":"10.14778\/3236187.3236200","type":"journal-article","created":{"date-parts":[[2018,9,10]],"date-time":"2018-09-10T12:12:28Z","timestamp":1536581548000},"page":"1482-1495","source":"Crossref","is-referenced-by-count":53,"title":["Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries"],"prefix":"10.14778","volume":"11","author":[{"given":"Shumo","family":"Chu","sequence":"first","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brendan","family":"Murphy","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jared","family":"Roesch","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alvin","family":"Cheung","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dan","family":"Suciu","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Apache Calcite Project. http:\/\/calcite.apache.org.  Apache Calcite Project. http:\/\/calcite.apache.org."},{"key":"e_1_2_1_2_1","unstructured":"Apache Drill Project. http:\/\/drill.apache.org.  Apache Drill Project. http:\/\/drill.apache.org."},{"key":"e_1_2_1_3_1","unstructured":"Apache Flink Project. https:\/\/flink.apache.org.  Apache Flink Project. https:\/\/flink.apache.org."},{"key":"e_1_2_1_4_1","unstructured":"Apache Hive Project. http:\/\/hive.apache.org.  Apache Hive Project. http:\/\/hive.apache.org."},{"key":"e_1_2_1_5_1","unstructured":"Apache Kylin Project. https:\/\/kylin.apache.org.  Apache Kylin Project. https:\/\/kylin.apache.org."},{"key":"e_1_2_1_6_1","unstructured":"Apache Phoenix Project. https:\/\/phoenix.apache.org.  Apache Phoenix Project. https:\/\/phoenix.apache.org."},{"key":"e_1_2_1_7_1","unstructured":"Bug 5673: Optimizer creates strange execution plan leading to wrong results. http:\/\/tinyurl.com\/hwwn53r.  Bug 5673: Optimizer creates strange execution plan leading to wrong results. http:\/\/tinyurl.com\/hwwn53r."},{"key":"e_1_2_1_8_1","unstructured":"MapD Database System. https:\/\/www.mapd.com.  MapD Database System. https:\/\/www.mapd.com."},{"key":"e_1_2_1_9_1","volume-title":"https:\/\/github.com\/querycert\/qcert\/blob\/a2e924042ad44d1cb8abc352411c8ece8529d1a2\/coq\/NRA\/Optim\/NRARewrite.v#L66","unstructured":"Q*Cert Proof of Selection Distributed over Union. https:\/\/github.com\/querycert\/qcert\/blob\/a2e924042ad44d1cb8abc352411c8ece8529d1a2\/coq\/NRA\/Optim\/NRARewrite.v#L66 . Q*Cert Proof of Selection Distributed over Union. https:\/\/github.com\/querycert\/qcert\/blob\/a2e924042ad44d1cb8abc352411c8ece8529d1a2\/coq\/NRA\/Optim\/NRARewrite.v#L66."},{"key":"e_1_2_1_10_1","unstructured":"Query featuring outer joins behaves differently in Oracle 12c. http:\/\/stackoverflow.com\/questions\/19686262.  Query featuring outer joins behaves differently in Oracle 12c. http:\/\/stackoverflow.com\/questions\/19686262."},{"key":"e_1_2_1_11_1","volume-title":"Foundations of Databases","author":"Abiteboul S.","year":"1995","unstructured":"S. Abiteboul , R. Hull , and V. Vianu . Foundations of Databases . Addison-Wesley , 1995 . S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2742797"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3035961"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3034786.3034796"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/358769.358784"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803397"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/153850.153856"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_2_1_20_1","volume-title":"Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries. CoRR, abs\/1802.02229","author":"Chu S.","year":"2018","unstructured":"S. Chu , A. Cheung , and D. Suciu . Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries. CoRR, abs\/1802.02229 , 2018 . S. Chu, A. Cheung, and D. Suciu. Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries. CoRR, abs\/1802.02229, 2018."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3058728"},{"key":"e_1_2_1_22_1","volume-title":"CIDR. www.cidrdb.org","author":"Chu S.","year":"2017","unstructured":"S. Chu , C. Wang , K. Weitz , and A. Cheung . Cosette: An automated prover for SQL . In CIDR. www.cidrdb.org , 2017 . S. Chu, C. Wang, K. Weitz, and A. Cheung. Cosette: An automated prover for SQL. In CIDR. www.cidrdb.org, 2017."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/303976.303992"},{"key":"e_1_2_1_25_1","volume-title":"A Guide to the SQL Standard","author":"Date C. J.","year":"1989","unstructured":"C. J. Date . A Guide to the SQL Standard , Second Edition. Addison-Wesley , 1989 . C. J. Date. A Guide to the SQL Standard, Second Edition. Addison-Wesley, 1989."},{"key":"e_1_2_1_26_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"CADE","author":"de Moura L. M.","year":"2015","unstructured":"L. M. de Moura , S. Kong , J. Avigad , F. van Doorn , and J. von Raumer . The lean theorem prover (system description) . In CADE , volume 9195 of Lecture Notes in Computer Science , pages 378 -- 388 . Springer , 2015 . L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The lean theorem prover (system description). In CADE, volume 9195 of Lecture Notes in Computer Science, pages 378--388. Springer, 2015."},{"key":"e_1_2_1_27_1","first-page":"459","volume-title":"VLDB","author":"Deutsch A.","year":"1999","unstructured":"A. Deutsch , L. Popa , and V. Tannen . Physical data independence, constraints, and optimization with universal plans . In VLDB , pages 459 -- 470 . Morgan Kaufmann , 1999 . A. Deutsch, L. Popa, and V. Tannen. Physical data independence, constraints, and optimization with universal plans. In VLDB, pages 459--470. Morgan Kaufmann, 1999."},{"key":"e_1_2_1_28_1","volume-title":"Chase & backchase: A method for query optimization with materialized views and integrity constraints. 01","author":"Deutsch A.","year":"2001","unstructured":"A. Deutsch , L. Popa , and V. Tannen . Chase & backchase: A method for query optimization with materialized views and integrity constraints. 01 2001 . A. Deutsch, L. Popa, and V. Tannen. Chase & backchase: A method for query optimization with materialized views and integrity constraints. 01 2001."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_2_1_30_1","unstructured":"Z. \u00c9ikand W. Kuich. Modern Automata Theory.  Z. \u00c9ikand W. Kuich. Modern Automata Theory ."},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-36285-1_14","volume-title":"ICDT","author":"Fagin R.","year":"2003","unstructured":"R. Fagin , P. G. Kolaitis , R. J. Miller , and L. Popa . Data exchange: Semantics and query answering . In ICDT , volume 2572 of Lecture Notes in Computer Science , pages 207 -- 224 . Springer , 2003 . R. Fagin, P. G. Kolaitis, R. J. Miller, and L. Popa. Data exchange: Semantics and query answering. In ICDT, volume 2572 of Lecture Notes in Computer Science, pages 207--224. Springer, 2003."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/38713.38723"},{"key":"e_1_2_1_33_1","volume-title":"Graphs, Dioids and Semirings: New Models and Algorithms","author":"Gondran M.","year":"2008","unstructured":"M. Gondran and M. Minoux . Graphs, Dioids and Semirings: New Models and Algorithms . Springer , 1 edition, 2008 . M. Gondran and M. Minoux. Graphs, Dioids and Semirings: New Models and Algorithms. Springer, 1 edition, 2008."},{"issue":"3","key":"e_1_2_1_34_1","first-page":"19","article-title":"The cascades framework for query optimization","volume":"18","author":"Graefe G.","year":"1995","unstructured":"G. Graefe . The cascades framework for query optimization . IEEE Data Eng. Bull. , 18 ( 3 ): 19 -- 29 , 1995 . G. Graefe. The cascades framework for query optimization. IEEE Data Eng. Bull., 18(3):19--29, 1995.","journal-title":"IEEE Data Eng. Bull."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265535"},{"key":"e_1_2_1_36_1","unstructured":"J. Gross M. Shulman A. Bauer P. L. Lumsdaine A. Mahboubi and B. Spitters. The HoTT libary in Coq. https:\/\/github.com\/HoTT\/HoTT.  J. Gross M. Shulman A. Bauer P. L. Lumsdaine A. Mahboubi and B. Spitters. The HoTT libary in Coq. https:\/\/github.com\/HoTT\/HoTT."},{"key":"e_1_2_1_37_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/978-3-319-63390-9_15","volume-title":"CAV (2)","author":"Grossman S.","year":"2017","unstructured":"S. Grossman , S. Cohen , S. Itzhaky , N. Rinetzky , and M. Sagiv . Verifying equivalence of spark programs . In CAV (2) , volume 10427 of Lecture Notes in Computer Science , pages 282 -- 300 . Springer , 2017 . S. Grossman, S. Cohen, S. Itzhaky, N. Rinetzky, and M. Sagiv. Verifying equivalence of spark programs. In CAV (2), volume 10427 of Lecture Notes in Computer Science, pages 282--300. Springer, 2017."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.14778\/3151113.3151116"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2588555.2594530"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/211414.211419"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142363"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.14778\/1920841.1920886"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/130283.130294"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/342009.335421"},{"key":"e_1_2_1_46_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-49257-7_4","volume-title":"ICDT","author":"Popa L.","year":"1999","unstructured":"L. Popa and V. Tannen . An equational chase for path-conjunctive queries, constraints, and views . In ICDT , volume 1540 of Lecture Notes in Computer Science , pages 39 -- 57 . Springer , 1999 . L. Popa and V. Tannen. An equational chase for path-conjunctive queries, constraints, and views. In ICDT, volume 1540 of Lecture Notes in Computer Science, pages 39--57. Springer, 1999."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322221"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132773"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/233269.233360"},{"key":"e_1_2_1_50_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book","year":"2013","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book , Institute for Advanced Study , 2013 . The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."},{"issue":"1","key":"e_1_2_1_51_1","first-page":"569","article-title":"Impossibility of an algorithm for the decision problem in finite classes","volume":"70","author":"Trakhtenbrot B.","year":"1950","unstructured":"B. Trakhtenbrot . Impossibility of an algorithm for the decision problem in finite classes . D. Akad. Nauk USSR , 70 ( 1 ): 569 -- 572 , 1950 . B. Trakhtenbrot. Impossibility of an algorithm for the decision problem in finite classes. D. Akad. Nauk USSR, 70(1):569--572, 1950.","journal-title":"D. Akad. Nauk USSR"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s007780050018"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_3"},{"key":"e_1_2_1_54_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-642-17511-4_24","volume-title":"LPAR (Dakar)","author":"Veanes M.","year":"2010","unstructured":"M. Veanes , N. Tillmann , and J. de Halleux. Qex: Symbolic SQL query explorer . In LPAR (Dakar) , volume 6355 of Lecture Notes in Computer Science , pages 425 -- 446 . Springer , 2010 . M. Veanes, N. Tillmann, and J. de Halleux. Qex: Symbolic SQL query explorer. In LPAR (Dakar), volume 6355 of Lecture Notes in Computer Science, pages 425--446. Springer, 2010."},{"key":"e_1_2_1_55_1","volume-title":"CIDR. www.cidrdb.org","author":"Wang J.","year":"2017","unstructured":"J. Wang , T. Baker , M. Balazinska , D. Halperin , B. Haynes , B. Howe , D. Hutchison , S. Jain , R. Maas , P. Mehta , D. Moritz , B. Myers , J. Ortiz , D. Suciu , A. Whitaker , and S. Xu . The Myria big data management and analytics system and cloud services . In CIDR. www.cidrdb.org , 2017 . J. Wang, T. Baker, M. Balazinska, D. Halperin, B. Haynes, B. Howe, D. Hutchison, S. Jain, R. Maas, P. Mehta, D. Moritz, B. Myers, J. Ortiz, D. Suciu, A. Whitaker, and S. Xu. The Myria big data management and analytics system and cloud services. In CIDR. www.cidrdb.org, 2017."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158144"}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3236187.3236200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T09:48:39Z","timestamp":1672220919000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3236187.3236200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":56,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2018,7]]}},"alternative-id":["10.14778\/3236187.3236200"],"URL":"https:\/\/doi.org\/10.14778\/3236187.3236200","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2018,7]]}}}