E-graphs, data structures commonly used for equational reasoning in formal methods, have recently been repurposed for program optimization in domains such as circuit design, floating point arithmetic, query optimization, and general-purpose compilers. E-graphs provide three key benefits in this context:

1. enabling non-committal rewriting that can represent the new and old program simultaneously.
2. efficiently storing and analyzing large families of structurally similar programs en masse.
3. separating the exploration of program alternatives from the cost-based selection of the best program.

Together, these benefits hint at the "holy grail" of extensible program optimization: the user simply supplies legal rules to manipulate the program, and the system magically optimizes it in the best way possible according to those rules. However, there are still key limitations that prevent this technique from being easily and generally applicable to program optimization. This Dagstuhl Seminar will bring together experts in software and hardware compilation, verification, program analysis, and program synthesis to align the research community around this vision of e-graphs as the basis for program optimization in various domains, and to bring the current state-of-the-art closer to that vision.

The seminar will explore four broad thrusts:

1. Program representation: Present e-graph techniques work equationally over algebraic (i.e. terms) representation of programs. The exact encoding can have a tremendous impact on the success of applying e-graphs to a problem. This thrust will explore novel program representations that are amenable to algebraic manipulation. Also, we will discuss how to lift this restriction to other kinds of program representations (i.e. graph-based).
2. Rewriting models: The most popular e-graph toolkits work bottom-up, simultaneously applying all transformations to all parts of the program in an iterated fashion. This is effective in some circumstances, but not in others. This part of the seminar will explore alternative paradigms that could allow the user to further control the expansion of the e-graph, leading to greater scalability. Potential methods include: scheduling languages, top-down rewriting, "garbage collection" of the search space, early pruning a la branch-and-bound, and cooperation with destructive/canonicalizing rewriting.
3. Contextual reasoning: A known limitation of current approaches is the fact that there is one big, global equivalence relation. This means reasoning or optimizing under contextual or hypothetical assumptions. This is needed of course in theorem proving, but also in software/hardware compilers (optimizing under path conditions), and query optimization (requiring physical properties like sortedness). There exists limited work on how to address this need in e-graphs, and none of it is widely implemented or used. This topic will aim to address this, so e-graph techniques can better apply in areas that require contextual reasoning.
4. Extraction: The big benefit of e-graphs for program optimization is that they allow you to defer your decision making, instead allow you to choose between different versions of a program at a later time. However, this program extraction phase is challenging in its own right. For certain cost functions, it is known to be NP-hard. This topic will explore how to approach this challenging problem with new datasets, approximations, and other novel techniques.

Creative Commons BY 4.0

George A. Constantinides, Chris Fallin, Michel Steuwer, and Max Willsey