When writing SQL queries, it is often convenient to use correlated subqueries. However, for the database engine, these correlated queries are very difficult to evaluate efficiently. The query optimizer will therefore try to eliminate the correlations, a process referred to as unnesting. Recent work has introduced a single pass top-down algorithm for unnesting arbitrary SQL queries. That work did not include a formal proof of correctness, though. In this work we provide the missing formalization by formally defining the operator semantics and proving that the unnesting algorithm is correct.

翻译：在编写SQL查询时，使用相关子查询通常非常方便。然而，对于数据库引擎而言，这些相关查询很难高效求值。因此，查询优化器会尝试消除相关性，这一过程被称为unnesting。近期研究提出了一种用于消除任意SQL查询相关性的单遍Top-Down算法，但该工作未包含形式化的正确性证明。本文通过形式化定义运算符语义并证明unnesting算法的正确性，提供了缺失的形式化基础。