HoTTSQL: Proving query rewrites with univalent SQL semantics
https://blog.acolyer.org/2017/10/05/hottsql-proving-query-rewrites-with-univalent-sql-semantics/ [blog.acolyer.org]
2017-10-07 03:12
Query rewriting is a vital part of SQL query optimisation, in which rewrite rules are applied to a query to transform it into forms with (hopefully!) a lower execution cost. Clearly when a query is rewritten we still want it to mean the same thing as the original – we call this semantic preserving. If you take Q1 and turn it into Q2, then for all database schemas and table instances Q1 and Q2 need to return the same results. Since query rewriting is used extensively in SQL engines, it may come as a surprise to you to learn that we don’t actually have proofs that many of the common rewrite rules actually are semantic preserving! Until now.