From: Gerwin Klein <kleing@unsw.edu.au>
Verification of Query Optimization Algorithms
by Lukas Stevens and Bernhard Stöckl
This formalization includes a general framework for query optimization consisting of the definitions of selectivities, query graphs, join trees, and cost functions. Furthermore, it implements the join ordering algorithm IKKBZ using these definitions. It verifies the correctness of these definitions and proves that IKKBZ produces an optimal solution within a restricted solution space.
https://www.isa-afp.org/entries/Query_Optimization.html
Enjoy!
Gerwin
Last updated: Jan 04 2025 at 20:18 UTC