CONCUR'18 Anode1
SQL 编码为 FOL，基础理论，无代码；
SIGMOD'22 WeTune2
SIGMOD2022 WeTune，王肇国等。
- Databend-【论文分享｜ SIGMOD'22】WeTune 自动发现和验证重写规则：https://zhuanlan.zhihu.com/p/630112740
- Gauss 松鼠会-WeTune：一种可以自动合成重写规则的规则生成器：https://www.zhihu.com/zvideo/1530486978957414400
当限制条件 C 为真时，原计划和目标计划恒等，即 \(Q_{src} \equiv Q_{dest}\)，此时可以进行查询重写。
该工作将 Query Plan Template 编码为 FOL。QPT 是一棵树，用于描述查询语句的抽象逻辑结构。
对我们工作的启发：从 QPT 入手
VLDB'18 U-semiring3
在本文中，我们提出了一种新的形式化方法和实现，用于推理 SQL 查询的等效性。我们的形式化方法 U-semiring 扩展了 SQL 的半环语义，具有无界求和和重复消除。U-semiring 仅使用很少的公理定义，因此可以使用 Lean 等证明助手轻松实现以进行自动查询推理。然而，它们足以使我们能够推理在袋子和集合上评估的复杂 SQL 查询，以及各种完整性约束。
Kartik Nagar and Suresh Jagannathan. Automated Detection of Serializability Violations Under Weak Consistency. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 41:1-41:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.41↩︎
Zhaoguo Wang, Zhou Zhou, Yicun Yang, Haoran Ding, Gansen Hu, Ding Ding, Chuzhe Tang, Haibo Chen, and Jinyang Li. 2022. WeTune: Automatic Discovery and Verification of Query Rewrite Rules. In Proceedings of the 2022 International Conference on Management of Data (SIGMOD '22). Association for Computing Machinery, New York, NY, USA, 94–107. https://doi.org/10.1145/3514221.3526125↩︎
Shumo Chu, Brendan Murphy, Jared Roesch, Alvin Cheung, and Dan Suciu. 2018. Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries. Proc. VLDB Endow. 11, 11 (July 2018), 1482–1495. https://doi.org/10.14778/3236187.3236200↩︎
