EGraphs as Ground Completion Talk and EGRAPHS 2024 notes
I’m back from Copenhagen! It was really fantastic time. Thanks everyone for the chats and saying you read my blog / enjoyed my talk! I really wish I had stayed for Thursday and Friday as I was still having great conversations. It wasn’t clear when I was booking if I would get any time from work, so I tried to hedge things a little. I looked into changing my flights around and it would’ve doubled the cost of my trip. Oh well, live and learn.
I rerecorded a version of my talk while I still remember roughly how to give it. Unfortunately, it seems the stream of my high energy audience version has a stuttering problem
The Big Takeaway From My Talk
Ground completion gives a canonical rewrite system that is as visualisable as regular egraphs, but has better scoping and is more ready for extensions. The standard egg example of ground equations describing multiply by two = shift by 1, and noticing a division cancellation becomes upon equational/knuth bendix completion the ground rewrite system
\[mul(a, two) \rightarrow shift(a, one)\] \[mul(a, one) \rightarrow a\] \[div(two, two) \rightarrow one\] \[div(shift(a, one), two) \rightarrow a\]Can be drawn as (representing rewrite arrows as red dotted arrows)
Whereas the egg diagram looks like
Note that
 The enodes in the egg diagram have eclasses as children, whereas the GRS egraph is actually about terms
 Red arrows connect things in the same eclass, but they are directed towards the better terms. This gives a useful and principled directionality internal to an eclass.
EGRAPHS 2024
Another great year!
You can see me hiding in the back there.
 The highlight may have been the slotted egraphs talk, which I actually missed (I was chatting in the hall but I watched it that night). I think they are really on to something. For my money, I just want a solution to alpha equivalence in the egraph, which this may be a functioning version of. I have a suspicion that their solution can be cast as ground nominal completion https://link.springer.com/chapter/10.1007/9783642315855_21 if that’s what you’re into. https://pldi24.sigplan.org/details/egraphs2024papers/10/SlottedEGraphs. https://github.com/memoryleak47/egraphsandbox Slots are wires. Maybe integrate the permutation union find (you can tag the dges of a union find with group elements https://www.philipzucker.com/unionfindgroupoid/)? This seems similar to why Kmett was thinking about such things anyway. He was doing something nominal. https://youtu.be/KxeHGcbh4c?t=1254
 The hyperegraphs talk was attacking some things along lines I have been musing about. I have not been going category theory, but I think there is an argument that we keep trying to model graphs (usually program graphical IRs) as terms by cutting them up in fairly arbitrary algebraic flavored ways. There is an possible indirection for graphs/hypergraphs analogous to that in the egraph. If I wanted to cut a little chunk out of a graph and replace it using a graph rewrite rule, I can keep both copies if I put a boundary eclass hyperedge around the region I’m cutting. Non overlapping graph/hypergraph rewriting can share a lot of structure in this way. For overlapping structure, you need to expand out / push this boundary enough that you can find your complete pattern. Maintaining this mushing around of hyperedge eclasses seems annoying. Recollecting up shared structure / “canonization” I think can be done greedily and imperfectly via something analogous to the FM algorithm for greedily improving partitioning. I think in their presentation they did not give any clues to how to implement such a thing, so the promise of “baked in structure” seems false without that. Maybe mathematically its baked in but that isn’t quite enough for my tastes. https://en.wikipedia.org/wiki/Fiduccia%E2%80%93Mattheyses_algorithm https://pldi24.sigplan.org/details/egraphs2024papers/9/EquivalenceHypergraphsEGraphsforMonoidalTheories
 The SpEQ paper is honestly shocking (in an impressive way). I would describe it as kind of like instruction selection for big kernels like MKL. The use case barely skirted around issues of alpha equivalence in the egraph. Rules are intrinsically alpha equivalent so that’s fine, but also because they weren’t generating new stuff. It also reminds me a bit of Jimmy Koppel’s code search YOGO https://www.jameskoppel.com/publication/yogo/
 Hardware continutes to be very intriguing. A lot of promise there. Clock gating. Data gaating. Transparent latch
 Test Set reduction. Interesting use case
 The monoidal category talk reminds me a lot of a line of work I was pursuing and actually brought me into egraphs Rewriting Monoidal Categories in the Browser with Egg
 The disequality talk I thought was quite enjoyable and illuminating. “Forbid” is a magic word for disequality in egraphs and was considered by Nelson. Disequality edges in the graph. Things you aren’t equal to is kind of a set/lattice like analysis you can tag. Maybe it would be nice to just have a pull request into egg putting this feature in there if its as easy to do as the slides suggest? https://pldi24.sigplan.org/details/egraphs2024papers/14/DisequalitiesinEGraphsAnExperiment. Would it be nice to reify equality edges in the diagram too? Is it not meaningful?
Other notes / thoughts from conference
 Max B is into serialization and hashing. The Ground completion egraph is easy to write down canononically, whereas the egg egraph it is not obvious (general graph hashing / isomorphism techniques?). Each rewrite rules is a tuple. Terms have an ordering to them. Write down the tuples in order. That is a canonical representation of the egraph that is hashable via the usual structural means. https://www.philipzucker.com/hashingmodulo/
 The GRS egraphs might be nice for the “use egraph to get full equational system” problem of QEL https://pldi23.sigplan.org/details/egraphs2023papers/8/PartiallyCompleteQuantifierElimination (they wanted to use it for fast quantifier elimination)
 Refinement in egraphs. A possibly a very useful thing if it can be straightened out. ALive2, refining optimizations. Good question from Zach
 Seems like someone in the UW crew as attacking the hyperreals. Fantastic!
 I’m excited for possible future collaborations with Max B and CF in more serious compiler work. Good convos.
 Z3 inside Z3 for hilbert choice
 JIT is interesating. Linearized control flow but with contexts coming from guards/asserts. Superposition on inline vs not in egraph a la Oliver?
 Cheney List copying
 Householder https://www.cs.princeton.edu/~zkincaid/ ? What was Zach talking about?
 Eva compiler for Reals. Daisy. Comparison of float32 vs float16 instead of attack reals? More useful even sometimes since the “spec” is some program people know works and we just want to reduce bitwidth for speed or something. Also if changing float size does something weird, something is fishy anyway.
 Bombe game https://store.steampowered.com/app/2262930/Bombe/. Is prolog like?
 Hydra https://users.cs.utah.edu/~regehr/generalizationoopsla24.pdf Hydra: Generalizing Peephole Optimizations with Program Synthesis
 “Coninductive” Egraphs. Useful for PEGs? Mark some things as object like identifiers. Observations go in ground completion egraph
head(s) > 3; tail(s) > s1
.Run automata minimization on them.  Solver for arbitrary bitvector length?
 Rudi thinks I should seriously bench mark bottom up ematching. It is important to have an outsider believe in something.
 Gotta get in on that sparse tensor shit
 SSI is kind of like ASSUME nodes https://dspace.mit.edu/bitstream/handle/1721.1/86578/48072795MIT.pdf
 Hyperreal Asbtract rewrite system and lyapunov functions? Insane talk.
 Refcells lambdas. Linear typing. Prolog lambdas. Unification variables are a “resource”
 Prolog continuations / CPS and Nat decuct > sequent calc
 Their geese are like ours, but wrong.
My Talk Abstract
Pdf here https://github.com/philzook58/egraphs2024talk/blob/main/egraphs2024_abstract.pdf
Introduction
Term simplification is a natural and intuitive concept. It can be used to both solve algebra problems and optimize compiler output.
A first simple but effective impulse is to treat simplification via greedy rewriting.
Like many heuristic greedy methods, it is possible that a locally greedy move can lead to globally suboptimal results. It is sometimes necessary to travel up the mountain to escape the valley. To fix this, some amount of breadth first or backtracking exploration is necessary.
The field of automated reasoning has been aware of and refining these notions for a long time.

Paramodulation [@NIEUWENHUIS2001371] is a breadth first technique for (possibly conditional) equational reasoning

Completion[@traatbook] is a method to convert an equational system to one with good guaranteed greedy rewriting properties. It can also be seen as equational reasoning with strong redundancy removal principles.

Superposition [@braniac] combines properties of completion and paramodulation.
Egraphs [@eggpaper] are a compact data structure for representing a collection of ground equations over terms and their congruence closure. They are an intuitively appealing technique for theorem proving and simplification. No small part of this intuition is provided by the bipartite graphical diagram of eclasses and enodes. There is a lower theoretical and technical barrier to entry in egraph rewriting than for navigating the complex automated reasoning literature. This conceptual simplicity has been essential for the egraph’s flourishing applications.
There is also a difference in attitude between the mainstream of the automated reasoning community and the egraphs community. The majority of the literature in automated reasoning is concerned with theorem proving problems. The egraph literature has a healthy contingent concerned with simplification/optimization/compiler problems. The egraph community wants a controllable quasi operational view of the search process and desire for completeness of the search does not override pragmatism. This is similar to the viewpoint of the Argonne school of automated reasoning [@ottermanual] [@wosautomated], which supported a more tweakable operational approach to automated reasoning.
This talk is about explaining some of the connections between different techniques and how they may give clues to fundamental problems in egraphs.
Union Finds as Completion
The union find is a key component of the egraph. It can be seen as an instance of completion [@groundegraph]. Indeed many algorithms, including Gaussian elimination, Grobner bases, resolution and others, can be viewed in this light.
A union find is a forest of equivalence classes. The pointers in the tree point upward to parents rather than downward to children. This can be viewed as a discrete dynamical system describing a convergent flow to a canonical member of the class. In other words, a convergent rewriting system.
For example, the following rewrite system is a representation of a union find where $b$ and $c$ are children of a canonical member $a$ and $e$ is a child of the canonical member $d$.
\(b \rightarrow a\) \(c \rightarrow a\) \(e \rightarrow d\)
Completion can be described as an inference rule system [@traatbook], orienting equations into rewrite rules and simplifying them. This simplification is a perspective on the path compression step in the union find.
The pieces of a simple union find algorithm can be dignified via reference to these rules.
class UF():
def __init__(self):
self.rules = {}
def find(self, x):
# `find` reduces x with respect
# to the current rules (x R> retval)
while self.rules.get(x) != None:
x = self.rules.get(x)
return x
def union(self, x, y):
# Do incremental completion starting with
# (E,R) == ({x = y}, self.rules )
x1 = self.find(x) # SIMPLIFY ( {x1 = y} , R)
y1 = self.find(y) # SIMPLIFY ( {x1 = y1}, R)
if x1 == y1: # TRIVIAL ({x1 = x1}, R)
return x1 # (Empty, self.rules)
else:
if x1 < y1: # the "term order"
x1,y1 = y1,x1 # swap
# ORIENT (empty, R U {x1 > y1})
self.rules[x1] = y1
return y1
def canon(self):
for lhs,rhs in self.rules.items():
self.rules[lhs] = self.find(rhs) # rsimplify
Egraphs as completion
Performing a regular completion procedure on ground terms is guaranteed to terminate. By putting the system in a flat canonical form, it is easier to see the correspondence with more familiar egraph notions.
The flattening transformation can be achieved by creating fresh ground symbols for every function application in the original set of equations.
For example,
\[foo(biz(baz), bar) = bar\]becomes
\[bar = e1\] \[baz = e2\] \[biz(e2) = e3\] \[foo(e3,e1) = e4\] \[e4 = e1\]With an appropriate ground term ordering that puts every $e$ less than any function symbol will orient the system into the form
\(bar \rightarrow e1\) \(baz \rightarrow e2\)
\[biz(e2) \rightarrow e3\] \[foo(e3,e1) \rightarrow e4\] \[e4 \rightarrow e1\]Completing a ground system of this sort will put it in a canonical form. The rewrite rules can be separated into two classes, those that rewrite enodes to eclasses and those that rewrite eclasses to other eclasses. The first represents the membership of enodes to their eclass and the second class represents a union find.
If we write $e$ as $q$, this becomes the definition of a tree automata as has been noted [@treeautomata]. Tree automata implicitly describe classes of trees using functional folds over finite state accumulators as acceptor functions, which can be described by tabulatable data. The ground rewriting point of view of egraphs is the same observation as identifying egraphs with tree automata but with a different emphasis of ideas.
The flattening transformation is not necessary for ground completion, but it does make the system more uniform. Notions of binding and context can be an impediment to this flattening transformation, so this complication may have a purpose.
Extraction
The idea of a term ordering has not made an explicit appearance in the modern egraphs literature to the author’s knowledge. Term ordering is a generalization of the notion of comparing terms for simplicity [@traatbook]. We typically want to rewrite a big term into a smaller one. With a completed ground rewrite system, running the system against the initial term will compute an equivalent smaller term. This is the analog of the egraph extraction process, and picking a term order picks the extraction goals. Giving symbols extraction weights corresponds to a similar notion that appears in knuth bendix ordering.
Ematching
The first component of egraph rewriting is to have an egraph. The second component is ematching.
An egraph implicitly represents a possibly infinite set of terms that are equivalent to terms inserted via the ground equations.
A ground completed rewrite system represents a possibly infinite set of terms that rewrites to something that is a right hand side of the system. Alternatively, the set is generated by running the rules backwards.
Ematching is trying to find a term in this set that matches a pattern. This can be described in the terminology of the GRS without explicit reference to egraphs [@ematchground].
Bottom up ematching is the simplest naivest method. One makes a nondeterministic guess to fill in variables in the pattern with a choice of right hand side in the GRS. Then one reduces the grounded pattern and see if reduces to a right hand side or not. Top down ematching can be achieved by narrowing the variables in the pattern according to current rewrite system. Every narrowing will ground out the pattern, since the rewrite system is ground.
Saturation
Saturation is not a unique property of egraph rewriting. Traditional automated reasoners are also saturating systems.
It is a known technique in the automated reasoning community that it is useful to separate clauses into at least two groups that are not treated symmetrically. Sometimes these are called unprocessed/processed or usable/set of support [@ottermanual]. Naive resolution or paramodulation considers every possibly pair of interaction between currently derived clauses. The givenclause algorithm is a form of seminaive evaluation that only further processes fresh clauses from the unprocessed set against the processed set.
Something quite similar to egraph rewriting can be made to occur by restricting a superposition prover to only allow superposition between a ground rewrite rule and a nonground rewrite rule. This is similar to some mixture of hyperresolution, URresolution, and set of support strategies [@wosautomated].
Hints for a Road Forward
There are a number of possible tantalizing expressivity extensions to the egraph. The extreme sharing and destruction of context in the egraph make many extensions hard to talk about. The connection back to term rewriting and automated reasoning sheds light on possible implementation methods.
Context
Superposition is a technique for equational theorem proving. It extends Knuth Bendix completion to equational clauses. A clause of terms $a \neq b \vee b = c$ can be seen as an implication $a = b \rightarrow b = c$.
Horn encodings [@hornformula] are a technique for getting context into pure completion solvers. It is similar in character to ASSUME nodes [@coward2023automating].
Another suggested technique for context is colored egraphs [@singher2023colored]. I am not aware of a similar notion in the automated reasoning literature.
Lambda
Recently superposition has been extended to support lambda terms [@bentkampsuperposition]. A restriction of this capability should be sufficient to implement an analog of egraph rewriting for lambda terms.
It is not clear that full lambda unification or matching is necessary or desirable. It depends on the application and performance trade offs. More limited but efficient forms of matching that nevertheless treat variable binding correctly such as Nominal unification [@nominal] or Miller patterm unification [@miller] may be preferred.
Backwards Reasoning
Egraph saturation is a bottom up technique analogous to datalog. A natural question is raised as to what a natural top down like prolog would look like.
Datalog and prolog can be viewed as incomplete strategies for resolution in a similar way that egglog [@egglog] and functional logic programming are incomplete strategies for superposition.
Understanding this connection may be useful in possible applications of egraph techniques to typeclass or trait resolution.
AC
The automated reasoning community has been aware of the issue of associativity and commutativity from the beginning. These rewrite rules are difficult to orient, commonplace, and very structural. There is a large literature on this subproblem and modern automated theorem such as E and Vampire have some intrinsic support for this.
Eager Rewriting
Demodulation is terminology used for eager rewriting in theorem provers. The ground rewrite system perspective of egraphs lends some clarity to the lack of completeness that may result.
Ematching in the egraph’s community refers to matching over an egraph. Ematching in the automated reasoning community refers to the more general mechanism of matching with regards to a background equational theory, often theories that are confluent and terminating. This is another approach to building in rewriting with respect to an a priori well behaved set of rewrite rules.
Universal Variables
Proving universal goals using egraphs requires some slight of hand and preprocessing. Standard automated reasoning techniques support true unification variables, which are an assertion of the universal applicability of the fact derived. They are scoped to their clause and are alpha renameable, which makes them distinct from the egraph’s equational constant symbols. Some degree of interemulation is possible.
Sketches and Hints
The two communities have separately invented similar notions of sketches [@sketch] and hints [@hints].
Conclusion
Egraph rewriting and other automated reasoning techniques are deeply interconnected. Neither is strictly better than the other and lessons can flow in both ways. The egraph has a intuitive appeal and by focusing on a subproblem is simpler to implement and hence fast. Automated reasoning systems implementing completion or superposition have a long history of theoretical and implementation refinement. It is seemingly conceptually simpler to extend these systems than to extend the highly shared and context destroying egraph, but perhaps a new efficient and expressive perspective can emerge by pumping insight between the two.
This material is based upon work supported by the under Grant No. and Grant No. . Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.
Talk Slides
Actual talk file here https://github.com/philzook58/egraphs2024talk/blob/main/egraphs_talk.ipynb I used RISE, a jupyter extension. It worked ok. Had to tweak some sizes and it still didn’t end up perfect. I didn’t end up having as much interactive code running as I thought. That was overly ambitious.
Egraphs and Automated Reasoning
Looking Back to Look Forward
Philip Zucker
June 22, 2024
The Main Points of The Talk
 Simplification & Completion
 Unionfind is Ground Atomic Completion
 EGraph is Ground Term Completion
 ? is Lambda, Context, Destructive
 Compilers from Automated Reasoners
In the Beginning…
💥 SIMPLIFICATION 💥
Greedy Simplification
 ex: $a + 0 \rightarrow a$
 Good
 Fast
 Simple
 Bad
 Rule Interaction / Phase Ordering ${a * 2 \rightarrow a \ll 1; (a*b)/b \rightarrow a }$
 Non termination $a + b \rightarrow b + a$
 Incompleteness / Suboptimality
EGraphs 🥚
 They’re Good
 Graphical, Simple
 Declarativeish
 Operationalish
 Fastish
 Many applications
 Usage Modes
 Proving:
Term > Term > Bool/Proof
 Simplifying:
Term > Term
 Proving:
\(a * 2 = a \ll 1\) \((a * 2) / 2 = a *(2 / 2) = a * 1 = a\)
Refinements
 Paramodulation (60s)  Go breadth first and conditional
 Completion (70s)  Make greedy good, remove redundancy
 Superposition (90s)  Combo
Completion
 Make Equations into “Good” Rules
 Terminating
 Confluent  No phase ordering problem
 Early Stopping
 Goal Driven
 Simplification Driven
Basic Completion
 Orient according to Term Order \([X * 2 = X \ll 1] \Rightarrow \{X * 2 \rightarrow X \ll 1\}\)
 Add critical pairs (CPs) as equations \(\{X * 2 \rightarrow X \ll 1; (X*Y)/Y \rightarrow X\} \Rightarrow\) \([(X \ll 1) / 2 = X]\)
 Reduce Equations \([a = b], \{a \rightarrow c\} \Rightarrow [c = b], \{a \rightarrow c\}\)
 Repeat
More Advanced Completion
Src: Baader and Nipkow
Twee
 Theorem prover for equational logic
 It is built around completion
 Optimized Haskell
 TPTP input
 CASC UEQ
%%file /tmp/shift.p
fof(shift, axiom, ![X] : mul(X,two) = shift(X, one)).
fof(cancel, axiom, ![X,N] : div(mul(X,N),N) = X).
fof(goal, conjecture, true = false).
Overwriting /tmp/shift.p
!twee /tmp/shift.p
Here is the input problem:
Axiom 1 (shift): mul(X, two) = shift(X, one).
Axiom 2 (cancel): div(mul(X, Y), Y) = X.
Goal 1 (goal): true = false.
1. mul(X, two) > shift(X, one)
2. div(mul(X, Y), Y) > X
3. div(shift(X, one), two) > X
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
mul(X, two) > shift(X, one)
div(mul(X, Y), Y) > X
div(shift(X, one), two) > X
RESULT: CounterSatisfiable (the conjecture is false).
The Main Points of The Talk
 Simplification & Completion
 Unionfind is Ground Atomic Completion
 EGraph is Ground Term Completion
 ? is Lambda, Context, Destructive
 Compilers from Automated Reasoners
Union Finds as Atomic Rewrite Systems
 Egraph ~ union find + hash cons
 Union find
 forest of equivalence classes
 Pointers up to parents
 Find = Convergent Dynamical System
 Convergent Dynamic System = Confluent Abstract Rewrite System
TRS  UF 

Run TRS  Find 
Add equation  Union 
R/L simplify  Compression 
Term Ordering  Tie Breaking 
%%file /tmp/unionfind.p
cnf(ax1, axiom, a = b).
cnf(ax2, axiom, b = c).
cnf(ax3, axiom, c = d).
cnf(ax4, axiom, d = e).
cnf(ax5, axiom, f = g).
cnf(false, conjecture, true = false).
Overwriting /tmp/unionfind.p
!twee /tmp/unionfind.p
Here is the input problem:
Axiom 1 (ax5): f = g.
Axiom 2 (ax1): a = b.
Axiom 3 (ax2): b = c.
Axiom 4 (ax4): d = e.
Axiom 5 (ax3): c = d.
Goal 1 (false): true = false.
1. g > f
2. b > a
3. c > a
4. d > e
5. e > a
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
b > a
c > a
d > a
e > a
g > f
RESULT: CounterSatisfiable (the conjecture is false).
import graphviz
def node(e):
#print(e, e.get_id())
return str(e.get_id())
def graphviz_of_z3(e, dot):
#label = "<head>" + e.decl().name() + " {" + "".join([ f"<p{n}>{n}" for n in range(e.num_args())]) + "}"
if e.num_args() == 0:
label = f'{{<head>{e.decl().name()}}}'
else:
label = f'{{<head>{e.decl().name()}{{{"".join([f"<p{n}>" for n in range(e.num_args())])}}}}}'
#print(label)
dot.node(node(e), label, shape="Mrecord") # id?
for n,c in enumerate(e.children()):
a,b = node(e) + ":p" + str(n) , node(c) + ":head"
if (a,b) not in dot.added_edges:
dot.added_edges.add((a,b))
dot.edge(a,b)
graphviz_of_z3(c, dot)
def show_rewrite(R):
dot = graphviz.Digraph()
dot.added_edges = set()
for l,r in R:
dot.edge(node(l) + ":head", node(r) + ":head", style="dashed", color="red")
graphviz_of_z3(l,dot)
graphviz_of_z3(r,dot)
return dot
from z3 import *
a,b,c,d,e,f,g = Consts("a b c d e f g", IntSort())
R = [
(b,a),
(c,a),
(d,a),
(e,a),
(g,f)
]
show_rewrite(R)
\(b \rightarrow a\) \(c \rightarrow a\) \(d \rightarrow a\) \(e \rightarrow a\) \(g \rightarrow f\)
%%file /tmp/unionfind.p
% Twee's "union find" is proof producing
cnf(ax1, axiom, a = b).
cnf(ax2, axiom, b = c).
cnf(ax3, axiom, c = d).
cnf(ax4, axiom, d = e).
cnf(ax5, axiom, f = g).
cnf(false, conjecture, a = e).
Overwriting /tmp/unionfind.p
!twee /tmp/unionfind.p
Here is the input problem:
Axiom 1 (ax5): f = g.
Axiom 2 (ax1): a = b.
Axiom 3 (ax2): b = c.
Axiom 4 (ax3): c = d.
Axiom 5 (ax4): d = e.
Goal 1 (false): a = e.
1. g > f
2. b > a
3. c > a
4. d > a
5. e > a
The conjecture is true! Here is a proof.
Axiom 1 (ax1): a = b.
Axiom 2 (ax2): b = c.
Axiom 3 (ax3): c = d.
Axiom 4 (ax4): d = e.
Goal 1 (false): a = e.
Proof:
[32ma[m
= [1m{ by axiom 1 (ax1) }[m
[32mb[m
= [1m{ by axiom 2 (ax2) }[m
[32mc[m
= [1m{ by axiom 3 (ax3) }[m
[32md[m
= [1m{ by axiom 4 (ax4) }[m
e
RESULT: Theorem (the conjecture is true).
The Main Points of The Talk
 Simplification & Completion
 Unionfind is Ground Atomic Completion
 EGraph is Ground Term Completion
 ? is Lambda, Context, Destructive
 Compilers from Automated Reasoners
EGraph is Ground Term Completion
 Egraph = Completed Reduced Ground Rewrite System
 Ground completion “solves” ground equalities
 Egraph “solves” ground equalities
TRS  Egraph 

Canonical Term  EClass 
R/Lsimplify  Canonization 
Run Rules  Extract 
Term Orders  Extract Objective 
KBO Weights  Weights 
%%file /tmp/groundshift.p
fof(shift, axiom, mul(a,two) = shift(a, one)).
fof(assoc, axiom, div(mul(a,two),two) = mul(a,div(two,two))).
fof(cancel, axiom, div(two,two) = one).
fof(unit_mul, axiom, mul(a,one) = a).
fof(cancel, axiom, start_term(q,q,q,q,q,q,q) = div(mul(a,two), two)).
fof(goal, conjecture, true = false).
Overwriting /tmp/groundshift.p
!twee /tmp/groundshift.p
Here is the input problem:
Axiom 1 (cancel): div(two, two) = one.
Axiom 2 (unit_mul): mul(a, one) = a.
Axiom 3 (shift): mul(a, two) = shift(a, one).
Axiom 4 (assoc): div(mul(a, two), two) = mul(a, div(two, two)).
Axiom 5 (cancel): start_term(q, q, q, q, q, q, q) = div(mul(a, two), two).
Goal 1 (goal): true = false.
1. div(two, two) > one
2. mul(a, one) > a
3. mul(a, two) > shift(a, one)
4. div(shift(a, one), two) > a
5. start_term(q, q, q, q, q, q, q) > a
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
mul(a, two) > shift(a, one)
mul(a, one) > a
div(two, two) > one
div(shift(a, one), two) > a
start_term(q, q, q, q, q, q, q) > a
RESULT: CounterSatisfiable (the conjecture is false).
BV = DeclareSort("BV")
mul = Function("*", BV, BV, BV)
shift = Function("\<\<", BV, BV, BV)
div = Function("/", BV, BV, BV)
a,one,two= Consts("a 1 2", BV)
start = Const("start", BV)
R = [
(mul(a, two) , shift(a, one)),
(mul(a, one) , a),
(div(two, two) , one),
(div(shift(a, one), two) , a),
#(start , a)
]
from IPython.display import SVG, display
display(show_rewrite(R))
show_rewrite(R).render("./egraph2.txt")
display(SVG(filename="./egraphs_1.svg"))
WAKEUP! THE MOST IMPORTANT SLIDE
\(mul(a, two) \rightarrow shift(a, one)\) \(mul(a, one) \rightarrow a\) \(div(two, two) \rightarrow one\) \(div(shift(a, one), two) \rightarrow a\)
Where are the Eclasses and Enodes?
 Flattening
 Introduce fresh constants for every term
 Make them less in term ordering
\(bar = e1\) \(baz = e2\) \(biz(e2) = e3\) \(foo(e3,e1) = e4\) \(e4 = e1\)
\[foo(biz(baz), bar) = bar\]\[bar \rightarrow e1\] \[baz \rightarrow e2\] \[biz(e2) \rightarrow e3\] \[foo(e3,e1) \rightarrow e4\] \[e4 \rightarrow e1\]
 Two types of rules
 $foo(e7,e4) \rightarrow e1$ = enode table
 $e3 \rightarrow e1$ = union find
 Observations:
 Not obviously possible for scoped terms. Slots? $e1(X,Y)$
 Completion is an egraph with Universal (forall) variables / first class rules
 Tree Automata $cons(q1, q2) \rightarrow q2$
Ematching
 Equality saturation
 Ematch into egraphs
 Add new equality
 Run rules in reverse to generate all equivalent terms
 Top down and bottom up
Bottom up Ematching
 The simplest ematching algorithm
 Completely guess each pattern var
 Build term corresponding to pattern
 Plays nicer
 Theories (Commutativity via sorting)
 Containers
 Grobner bases?
 Destructive rules?
 Perhaps related to aegraph
Strategies
$\frac{A \lor B \quad \neg A \lor C}{B \lor C} $
 Incomplete but pragmatic limitations on resolution
 Set of Support  Rules vs EGraph
 Prolog
 Datalog ~ Hyperresolution + URresolution
Prop  Equational 

Resolution  Paramodulation 
Ordered Resolution  Superposition 
?  Completion 
Ground Ordered Resolution  Egraph / Ground Completion / Ground Superposition 
Prolog  Functional Logic Programming 
Datalog  Egglog 
ASP  ? 
Lambda Prolog  ? 
Hypothetical Datalog  ? 
Minikanren  ? 
The Main Points of The Talk
 Simplification & Completion
 Unionfind is Ground Atomic Completion
 EGraph is Ground Term Completion
 ? is Lambda, Context, Destructive
 Compilers from Automated Reasoners
Mysteries and Promises
 Context
 Lambdas
 Destructive
Context
 Twee
 Efficient encodings of firstorder Horn formulas in equational logic  Claessen & Smallbone
 In Twee today.
 Similar to ASSUME nodes
 Ground Superposition is a contextual egraph
 Negative literal ~ context
 Terminating but possibly explosive
Lambda
 Complete and Efficient HigherOrder Reasoning via LambdaSuperposition  Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, and Uwe Waldmann
 Zipperposition and E
 A CombinatorBased Superposition Calculus for HigherOrder Logic  Ahmed Bhayat, Giles Reger
 Vampire
 Lambda Free Higher Order Logic (LFHOL)
Destructive Rewriting
 Combination Problems (Chapter 9 TRAAT)
 Under what conditions does completion of Ground Eq + Rules stay well behaved?
 Term Ordering of destructive rules probably informs how ground should work
 Two senses of “Ematching”
The Main Points of The Talk
 Union find EGraph $\leftrightarrow$ Ground Atomic Completion
 Clues: Lambda, Context, Destructive
 Automated Reasoning $\rightarrow$ Compilers
 Fast Implementation?
 Simplifier Oriented
Term > Term
Thank You
 Abstract https://github.com/philzook58/egraphs2024talk/blob/main/egraphs2024.pdf
 Blog posts:
 References
 Term Rewriting and All That (TRAAT)
 Handbook of Automated Reasoning
 Automated Reasoning: Introduction and Applications
%%file /tmp/context.p
% Twee as a contexual egraph/union find
fof(shift, axiom, (a = b) => b = c).
fof(cancel, axiom, c = d ).
fof(cancel, axiom, e = f ).
fof(goa,conjecture, true = false).
Overwriting /tmp/context.p
!twee /tmp/context.p
Here is the input problem:
Axiom 1 (cancel): e = f.
Axiom 2 (cancel): c = d.
Axiom 3 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
Axiom 4 (shift): ifeq(a, b, b, c) = c.
Goal 1 (goa): true = false.
1. f > e
2. c > d
3. ifeq(X, X, Y, Z) > Y
4. ifeq(a, b, b, d) > d
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
c > d
f > e
ifeq(X, X, Y, Z) > Y
ifeq(a, b, b, d) > d
RESULT: CounterSatisfiable (the conjecture is false).
def simplify1(x):
match x:
case ("add", ("const", m), ("const", n)):
return ("const", m + n)
case ("add", ("const", 0), y)  ("add", y, ("const", 0)):
return y
case _:
return x
def simplify(expr):
match expr:
case ("add", x, y):
return simplify1(("add", simplify(x), simplify(y)))
case _:
return simplify1(expr)
simplify(("add", ("const", 3), ("const", 4)))
('const', 7)
class UF():
def __init__(self):
self.rules = {}
def find(self, x):
# `find` reduces x with respect to the current rules (x R> retval)
while self.rules.get(x) != None:
x = self.rules.get(x)
return x
def union(self, x, y):
# Do incremental completion starting with
# (E,R) == ({x = y}, self.rules )
x1 = self.find(x) # SIMPLIFY ( {x1 = y} , R)
y1 = self.find(y) # SIMPLIFY ( {x1 = y1}, R)
if x1 == y1: # TRIVIAL ({x1 = x1}, R)
return x1 # (Empty, self.rules)
else:
if x1 < y1: # the "term order"
x1,y1 = y1,x1 # swap
self.rules[x1] = y1 # ORIENT (empty, R U {x1 > y1})
return y1
def canon(self):
for lhs,rhs in self.rules.items():
self.rules[lhs] = self.find(rhs) # rsimplify
Tree Automata
 Strings ~ single argument terms $aaabb = a(a(a(a(b(b(\epsilon))))))$
 Term rewriting formulation of DFA
 $a^b^ = {a(q1) \rightarrow q1, a(q0) \rightarrow q1, b(q0) \rightarrow q0}$
 $a(a(a(a(b(b(q0)))))) \rightarrow^? q1$
 Generalizes to Tree. Finite State Folds
 Call $q1$ $e1$ and we have a flattened egraph
Src: Blanchette
%%file /tmp/groundshift.p
fof(e, axiom, a = e0).
fof(e, axiom, two = e1).
fof(e, axiom, mul(a,two) = e2).
fof(e, axiom, div(mul(a,two),two) = e3).
fof(e, axiom, one = e4).
fof(e, axiom, shift(a, one) = e5).
fof(e, axiom, div(two,two) = e6).
fof(e, axiom, mul(a, one) = e7).
fof(shift, axiom, mul(a,two) = shift(a, one)).
fof(assoc, axiom, div(mul(a,two),two) = mul(a,div(two,two))).
fof(cancel, axiom, div(two,two) = one).
fof(unit_mul, axiom, mul(a,one) = a).
fof(cancel, axiom, start_term(q,q,q,q,q,q,q) = div(mul(a,two), two)).
fof(goal, conjecture, true = false).
Overwriting /tmp/groundshift.p
!twee /tmp/groundshift.p
Here is the input problem:
Axiom 1 (e): one = e4.
Axiom 2 (e): a = e0.
Axiom 3 (e): two = e1.
Axiom 4 (e): shift(a, one) = e5.
Axiom 5 (e): div(two, two) = e6.
Axiom 6 (cancel): div(two, two) = one.
Axiom 7 (e): mul(a, one) = e7.
Axiom 8 (unit_mul): mul(a, one) = a.
Axiom 9 (e): mul(a, two) = e2.
Axiom 10 (shift): mul(a, two) = shift(a, one).
Axiom 11 (e): div(mul(a, two), two) = e3.
Axiom 12 (assoc): div(mul(a, two), two) = mul(a, div(two, two)).
Axiom 13 (cancel): start_term(q, q, q, q, q, q, q) = div(mul(a, two), two).
Goal 1 (goal): true = false.
1. one > e4
2. a > e0
3. two > e1
4. shift(e0, e4) > e5
5. div(e1, e1) > e6
6. e6 > e4
7. mul(e0, e4) > e7
8. e7 > e0
9. mul(e0, e1) > e2
10. e5 > e2
11. div(e2, e1) > e3
12. e3 > e0
13. start_term(q, q, q, q, q, q, q) > e0
Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
a > e0
two > e1
e3 > e0
one > e4
e5 > e2
e6 > e4
e7 > e0
mul(e0, e1) > e2
mul(e0, e4) > e0
div(e1, e1) > e4
div(e2, e1) > e0
shift(e0, e4) > e2
start_term(q, q, q, q, q, q, q) > e0
RESULT: CounterSatisfiable (the conjecture is false).
BV = DeclareSort("BV")
mul = Function("*", BV, BV, BV)
shift = Function("\<\<", BV, BV, BV)
div = Function("/", BV, BV, BV)
a,one,two= Consts("a 1 2", BV)
e0,e1,e2,e3,e4,e5,e6,e7 = Consts("e0 e1 e2 e3 e4 e5 e6 e7", BV)
start = Const("start", BV)
R = [
(a, e0),
(two, e1),
(e3, e0),
(one,e4),
(e5,e2),
(e6,e4),
(e7,e0),
(mul(e0,e1),e2),
(mul(e0,e4), e0),
(div(e1,e1),e4),
(div(e2,e1), e0),
(shift(e0,e4), e2),
#(start, e0)
]
show_rewrite(R)
%%file /tmp/shift.p
fof(shift, axiom, ![X] : mul(X,two) = shift(X, one)).
fof(assoc, axiom, ![X,Y,Z]: div(mul(X,Y), Z) = mul(X, div(Y,Z))).
fof(cancel, axiom, ![X]: div(X,X) = one).
fof(mul_one, axiom, ![X]: mul(X,one) = X).
fof(goal, conjecture, true = false).
Overwriting /tmp/shift.p