带空值的SQL的形式化
A Formalization of SQL with Nulls
摘要：
SQL是世界上最流行的声明性语言，是数十亿美元数据库行业的基础。虽然SQL已经标准化，但完整的标准是基于模糊的自然语言，而不是正式的规范。商业SQL实现以不同的方式解释标准，因此，给定相同的输入数据，相同的查询可以根据它运行的SQL系统产生不同的结果。即使对于特定的系统，SQL的所有广泛使用的功能的机械检查形式化仍然是一个开放的问题。缺乏一个良好理解的形式化语义使得验证数据库实现的可靠性非常困难。尽管SQL片段的形式化语义在过去已经设计好了，但它们通常不支持集合和包操作、横向连接、嵌套子查询，以及至关重要的空值。空值使SQL的语义复杂化，其方式与其他程序设计语言中的空指针或副作用类似。由于某些SQL查询在没有空值的情况下是等价的，但当应用于包含不完整数据的表时会产生不同的结果，因此忽略空值的语义能够证明在现实数据库中不合理的查询等价性。支持所有上述功能的SQL的正式语义最近才被提出。在本文中，我们报告我们的机械化SQL语义涵盖集/袋操作，横向连接，嵌套的子查询，空值，写在Coq证明助手，并描述了关键元属性的验证。此外，我们能够使用相同的框架来形式化平面关系演算（具有空值）的语义，并显示其范式到SQL的认证翻译。
英文摘要：
SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL's semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
