A Formalization of Top-Down Unnesting
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866929616938074112 |
|---|---|
| author | Neumann, Thomas |
| author_facet | Neumann, Thomas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_04294 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Formalization of Top-Down Unnesting Neumann, Thomas Databases 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. |
| title | A Formalization of Top-Down Unnesting |
| topic | Databases |
| url | https://arxiv.org/abs/2412.04294 |