SHF: Medium: Next Generation Equality Saturation by way of Datalog

SHF：中：通过数据记录实现下一代平等饱和度

• 批准号: 2312195
• 负责人: Zachary Tatlock
• 金额: $ 80万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2312195&HistoricalAwards=false
• 关键词: SHF; Medium; Next; Generation; Equality

A common challenge faced by all programming technology, including optimizing compilers, query optimizers, theorem provers, and model checkers, is the ability to reason about "term equivalence" -- that is, when one program is equivalent to another. Optimizing compilers seek to replace one sequence of instructions with another equivalent sequence that executes faster. Structured Query Language (SQL) query optimizers start from a query plan and search for an equivalent plan with lowest cost, and theorem provers need to infer equivalences between expressions to prove mathematical equations. Checking the equivalence of two expressions is one of the fundamental problems in computer science. The project's novelties are building a new framework for checking equivalence, by using a technique called equality saturation. Instead of rewriting a term to a new one and forgetting the old one, equality saturation keeps all equivalent terms in a single, compact representation. The project's impacts are developing new technology for checking equivalence that will impact compilers, query optimizers, and theorem provers, by improving their ability to reason about, and to optimize expressions.Equality saturation relies on a compact representation of a set of expressions using an E-Graph, where equivalent expressions are grouped into E-Classes, and individual operators are represented by E-Nodes. At the core of the approach is a fixpoint computation of the closure of a given expression under a specified set of rules and under equality. The project pursues three thrusts. The first thrust extends equality saturation with Datalog rules. The project exploits the fact that datalog is a query language that is also based on a fixpoint semantics, and builds a novel framework that allows datalog rules to be combined with equality assertions, in a unified way. In the second thrust the project conducts a theoretical investigation of the conditions that ensure termination of equality saturation. This problem has been studied independently under various aspects by the term rewriting community, the chase community, and the tree automata community; this project adapts those theoretical results to equality saturation. Finally, in the third thrust, the project creates new optimization techniques for equality saturation in order to improve its performance. These optimizations will be inspired by database query optimization techniques, such as worst-case optimal joins, semi-naive evaluation, and multiquery optimization.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

所有编程技术（包括优化编译器、查询优化器、定理证明器和模型检查器）面临的一个共同挑战是推理“术语等价”的能力，即一个程序何时与另一个程序等价。 优化编译器寻求用执行速度更快的另一等效序列替换一个指令序列。结构化查询语言（SQL）查询优化器从查询计划开始，搜索成本最低的等效计划，定理证明者需要推断表达式之间的等价性以证明数学方程。 检查两个表达式的等价性是计算机科学的基本问题之一。 该项目的新颖之处在于通过使用一种称为“相等饱和度”的技术来构建一个用于检查等效性的新框架。 等式饱和不会将一项重写为新项并忘记旧项，而是将所有等效项保留在一个紧凑的表示中。 该项目的影响是开发用于检查等价性的新技术，这将通过提高编译器、查询优化器和定理证明器的推理和优化表达式的能力来影响编译器、查询优化器和定理证明器。等式饱和依赖于使用 E 的一组表达式的紧凑表示-Graph，其中等效表达式被分组为 E 类，各个运算符由 E 节点表示。 该方法的核心是在一组指定规则和相等条件下给定表达式闭包的定点计算。 该项目追求三个主旨。 第一个推动力通过数据记录规则扩展了平等饱和度。 该项目利用了数据记录是一种基于定点语义的查询语言这一事实​​，并构建了一个新颖的框架，允许数据记录规则以统一的方式与相等断言相结合。 在第二个重点中，该项目对确保终止平等饱和的条件进行了理论研究。 这个问题已经由术语重写社区、追逐社区和树自动机社区在各个方面进行了独立研究；该项目使这些理论结果适应平等饱和。 最后，在第三个重点中，该项目创建了新的等式饱和优化技术，以提高其性能。 这些优化将受到数据库查询优化技术的启发，例如最坏情况最优连接、半朴素评估和多查询优化。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优势和更广泛的评估进行评估，被认为值得支持。影响审查标准。