Better Together: Unifying Datalog and Equality Saturation
Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey
Programming Language Design and Implementation 2023
Abstract
We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, it supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, it supports term rewriting, efficient congruence closure, and extraction of optimized terms.
We identify two recent applications – a unification-based pointer analysis in Datalog and an EqSat-based floating-point term rewriter – that have been hampered by features missing from Datalog but found in EqSat or vice-versa. We evaluate egglog by reimplementing those projects in egglog. The resulting systems in egglog are faster, simpler, and fix bugs found in the original systems.
BibTeX
@article{2023-pldi-egglog,
title = {Better Together: Unifying Datalog and Equality Saturation},
author = {Yihong Zhang and Yisu Remy Wang and Oliver Flatt and David Cao and Philip Zucker and Eli Rosenthal and Zachary Tatlock and Max Willsey},
journal = {Proceedings of the ACM on Programming Languages},
number = {PLDI},
year = {2023},
publisher = {Association for Computing Machinery},
url = {https://doi.org/10.1145/3591239},
doi = {10.1145/3591239},
}