2023/04/10 by Yihong Zhang, Yisu Remy Wang, Zhang, Yihong +13 · 2 voices · 17 citations
Computer Science · #Artificial intelligence #Computer science #Concurrency #Datalog #Formal Methods in Verification #Logic, programming, and type systems #Pointer (user interface) #Programming language #Rewriting #Security and Verification in Computing #Theoretical computer science #Unification
paper · pdf · doi:10.48550/arxiv.2304.04332
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2023/04/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.