Equality saturation is an emerging technique for program and query optimization developed in the programming language community. It performs term rewriting over an E-graph, a data structure that compactly represents a program space. Despite its popularity, the theory of equality saturation lags behind the practice. In this paper, we define a fixpoint semantics of equality saturation based on tree automata and uncover deep connections between equality saturation and the chase. We characterize the class of chase sequences that correspond to equality saturation. We study the complexities of terminations of equality saturation in three cases: single-instance, all-term-instance, and all-E-graph-instance. Finally, we define a syntactic criterion based on acyclicity that implies equality saturation termination.

翻译：等式饱和是编程语言社区开发的一种新兴的程序与查询优化技术。它通过在E图（一种紧凑表示程序空间的数据结构）上执行项重写来实现优化。尽管该技术已得到广泛应用，但其理论基础仍滞后于实践。本文基于树自动机定义了等式饱和的不动点语义，并揭示了等式饱和与追逐之间的深层联系。我们刻画了与等式饱和相对应的追逐序列类别。研究了等式饱和在三种情况下的终止复杂性：单实例、全项实例和全E图实例。最后，我们定义了一种基于无环性的语法准则，该准则可保证等式饱和的终止性。