HoTTSQL：证明具有单价SQL语义的查询重写
HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics
摘要：
每个数据库系统都包含一个执行查询重写的查询优化器。不幸的是，开发查询优化器仍然是一项极具挑战性的任务。部分挑战来自于查询语言的复杂性和丰富特性，这使得重写规则的推理变得困难。在本文中，我们提出了一个机器可检查的指称语义的SQL，事实上的语言为关系数据库，严格验证重写规则。与以前提出的非机械化或仅涵盖少量SQL语言功能的语义不同，我们的语义涵盖了SQL的所有主要功能，包括包，相关子查询，聚合和索引。我们的机械化语义，称为HoTTSQL，是基于K-关系和同伦类型论，其中我们表示关系作为数学函数从元组到单价类型。我们已经在Coq中实现了HoTTSQL，它只需要不到300行代码，并且已经证明了广泛的SQL重写规则，包括来自数据库研究文献的规则（例如，魔术集重写）和真实世界的查询优化器（例如，子查询消除）。这些重写规则中有几条以前从未被证明是正确的。此外，虽然查询等价性通常是不可判定的，但我们已经使用HoTTSQL实现了一个自动决策过程，用于合取查询：一个经过充分研究的可判定SQL片段，包含许多真实世界的查询。
英文摘要：
Every database system contains a query optimizer that performs query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes from the intricacies and rich features of query languages, which makes reasoning about rewrite rules difficult. In this paper, we propose a machine-checkable denotational semantics for SQL, the de facto language for relational database, for rigorously validating rewrite rules. Unlike previously proposed semantics that are either non-mechanized or only cover a small amount of SQL language features, our semantics covers all major features of SQL, including bags, correlated subqueries, aggregation, and indexes. Our mechanized semantics, called HoTTSQL, is based on K-Relations and homotopy type theory, where we denote relations as mathematical functions from tuples to univalent types. We have implemented HoTTSQL in Coq, which takes only fewer than 300 lines of code and have proved a wide range of SQL rewrite rules, including those from database research literature (e.g., magic set rewrites) and real-world query optimizers (e.g., subquery elimination). Several of these rewrite rules have never been previously proven correct. In addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using HoTTSQL for conjunctive queries: a well-studied decidable fragment of SQL that encompasses many real-world queries.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
