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

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.