Reproduce “Better Together: Unifying Datalog and Equality Saturation” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey
From the University of Washington, `egglog` is a new fixpoint reasoning system that unifies Datalog and Equality Saturation by integrating built-in equality and extensible merge expressions within a Datalog-like language. This system demonstrated a 4.96x speedup over sound Datalog baselines for points-to analysis and enabled sound rewrite rules for the Herbie floating-point optimizer, often finding more accurate programs.
Key insights
- Unifying Datalog's compositional semantic analysis with EqSat's efficient equational reasoning within a single fixpoint system is feasible and beneficial.
- Native, efficient handling of equivalence relations (like union-find) within a Datalog-like framework eliminates the need for complex, often unsound, workarounds.
- Flexible conflict resolution via user-defined "merge expressions" is crucial for supporting both congruence closure and lattice-based analyses within a unified functional database model.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.