.png){kind=icon}
返回
HoTTSQL: proving query rewrites with univalent SQL semantics
.png){kind=icon}
OA
AI
DOI：10.1145/3140587.3062348.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
每个数据库系统都包含一个执行查询重写的查询优化器。然而，开发查询优化器仍然是一项极具挑战性的任务。部分挑战源于查询语言本身的复杂性和丰富特性，这使得对重写规则的推理变得困难。在本文中，我们提出了一种机器可检验的指称语义，用于SQL（关系数据库的事实标准语言），以严格验证重写规则。与以往提出的要么非机械化、要么仅涵盖少量SQL语言特性的语义不同，我们的语义涵盖了SQL的所有主要特性，包括包、相关子查询、聚合和索引。我们的机械化语义称为HoTT SQL，基于K-Relations和同伦类型理论，其中我们将关系表示为从元组到单态类型的数学函数。我们已在Coq中实现了HoTTSQL，其代码量不足300行，并且已证明了一系列SQL重写规则，包括来自数据库研究文献（如magic set重写）和实际查询优化器（如子查询消除）的规则。其中一些重写规则此前从未被证明正确。此外，尽管查询等价性通常不可判定，我们已使用HoTTSQL实现了一个自动判定过程，用于合取查询：一种涵盖许多实际查询的可判定SQL子集。
期刊
暂无期刊信息
机构
暂无机构信息
引用论文
暂无论文信息