#egraph — Public Fediverse posts

I have been thinking a lot about e-graph lately, mainly to understand what "really is" an #egraph and give precise mathematical meaning to its expressions, which would facilitate reasoning about more complex structure with in e-graph without resorting to implementation details.

My proposal is that e-graph is a generative system, that is a coalgebra with the form 𝑋→𝑃₊(𝐹(𝑋)) where the states 𝑋 are e-classes, and the signature is a composition of two distinct component: the non-empty power set monad 𝑃₊ because each e-class contains multiple e-nodes, and the polynomial functor 𝐹 which is the standard functor that generates expressions over function symbols: 𝐹(𝑋)=Σ₀+Σ₁×𝑋+Σ₂×𝑋×𝑋 + …

This is similar to the modified tree automata definition given by Suciu, Wang, and Zhang in 2025: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.11

(Note: depends on your use case, this coalgebraic definition can be too premisive, as it do not guarantee an e-class to have an extraction.
To require e-class to have expression, we can restrict it to be a subcoalgebra to its initial algebra, which is also its final colagebra, in the Keisli category.)

Except, coalgebra of this form, or more generally 𝑋−>𝑀(𝐹(𝑋)) where 𝑀 is a monad, and 𝐹 is a polynomial functor is extensively studied under the name "generative system", originally intended to give trace semantics to general transition systems:
- https://arxiv.org/abs/0710.2505v1
- https://academic.oup.com/logcom/article/31/6/1482/6355531
- https://www.sciencedirect.com/science/article/pii/S0022000014001676

Many of the e-graph operations: merging (coequalizer), rebuilding (not entirely sure, but feels doable), extraction (lax coalgebra hom into expressions), and semantic interpretation, seems to all correspond to standard categorical objects.

I will be giving a talk at the #egraph workshop at @pldi on my collaborative work with Sam Coward, Philip Zucker (@sandmouth), and Alexandra Silva (@xanovsky) on incorporating fixpoint equation into e-graph.

This is a very interesting topic:
- Practically, we turn "recursive program" into a first-class citizen of e-graph, allowing users to reason about control-flow and (potentially infinite) data-flow natively without much encoding.
- Theoretically, this work has potential connection to exciting fields like iteration theory and bialgebraic semantics. Many of our elementary proof constructions look very similar to standard constructions in these fields.

The resulting framework, although general and simple on the surface, has a lot of interesting and subtle challenges.
We are (hopefully) very close to wrapping up this project, so I will be presenting a work in progress that should be reasonably similar to the final result :)

I will be giving a talk at the #egraph workshop at @pldi on my collaborative work with Sam Coward, Philip Zucker (@sandmouth), and Alexandra Silva (@xanovsky) on incorporating fixpoint equation into e-graph.

This is a very interesting topic:
- Practically, we turn "recursive program" into a first-class citizen of e-graph, allowing users to reason about control-flow and (potentially infinite) data-flow natively without much encoding.
- Theoretically, this work has potential connection to exciting fields like iteration theory and bialgebraic semantics. Many of our elementary proof constructions look very similar to standard constructions in these fields.

The resulting framework, although general and simple on the surface, has a lot of interesting and subtle challenges.
We are (hopefully) very close to wrapping up this project, so I will be presenting a work in progress that should be reasonably similar to the final result :)

[New Blog Post] A Slotted Hash Cons for Alpha Invariance https://www.philipzucker.com/slotted_hash_cons/ #hashing #egraph #lambda

[New Blog Post] A Slotted Hash Cons for Alpha Invariance https://www.philipzucker.com/slotted_hash_cons/ #hashing #egraph #lambda

[New Blog Post] Brute E-Graphs Modulo Theories 2: Extraction, Proofs, and Context #egraph #logic https://www.philipzucker.com/egraph-mt2/

[New Blog Post] Brute E-Graphs Modulo Theories 2: Extraction, Proofs, and Context #egraph #logic https://www.philipzucker.com/egraph-mt2/

[New Blog Post] Coset Enumeration using Equality Saturation https://www.philipzucker.com/coset_enum_egraph/ #egraph #grouptheory #algebra

[New Blog Post] Towards an AC Egraph: Groebner, Graver and Ground Multiset Rewriting https://www.philipzucker.com/multiset_rw/ #egraph

[New Blog Post] Towards an AC Egraph: Groebner, Graver and Ground Multiset Rewriting https://www.philipzucker.com/multiset_rw/ #egraph

[New Blog Post] Acyclic Egraphs and Smart Constructors https://philipzucker.com/smart_constructor_aegraph/ #egraph #compiler

[New Blog Post] Acyclic Egraphs and Smart Constructors https://philipzucker.com/smart_constructor_aegraph/ #egraph #compiler

[New Blog Post] Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas https://philipzucker.com/coegraph/ #egraph #logic #automatedreasoning

[New Blog Post] Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas https://philipzucker.com/coegraph/ #egraph #logic #automatedreasoning

[New Blog Post] Gauss and Groebner Egraphs: Intrinsic Linear and Polynomial Equations https://philipzucker.com/linear_grobner_egraph/ #logic #egraph #sympy

[New Blog Post] Gauss and Groebner Egraphs: Intrinsic Linear and Polynomial Equations https://philipzucker.com/linear_grobner_egraph/ #logic #egraph #sympy

[New Blog Post] Conditional Simplification of Z3py Expressions with Egglog https://philipzucker.com/egglog_z3_simp/ #logic #python #egraph

[New Blog Post] Conditional Simplification of Z3py Expressions with Egglog https://philipzucker.com/egglog_z3_simp/ #logic #python #egraph

[New Blog Post] EGRAPHS 2024 submission: E-graphs and Automated Reasoning https://philipzucker.com/egraph2024_talk/ #egraph #pldi

[New Blog Post] EGRAPHS 2024 submission: E-graphs and Automated Reasoning https://philipzucker.com/egraph2024_talk/ #egraph #pldi

Looking forward to the EGRAPHS community call lightning talks tomorrow...

https://egraphs.org/meeting/2024-03-21-lightning-talks

Wish me luck trying in explaining this chart of optimizing scikit-learn with numba using egraphs in ten minutes 🫣

https://egglog-python.readthedocs.io/latest/explanation/2024_03_17_community_talk.html

#python #opensource #egraph

Looking forward to the EGRAPHS community call lightning talks tomorrow...

https://egraphs.org/meeting/2024-03-21-lightning-talks

Wish me luck trying in explaining this chart of optimizing scikit-learn with numba using egraphs in ten minutes 🫣

https://egglog-python.readthedocs.io/latest/explanation/2024_03_17_community_talk.html

#python #opensource #egraph

[New Blog Post] Bottom Up Egraph Ematching Plays Nicer with Theories (AC, etc) https://philipzucker.com/bottom_up/ #egraph #python #termrewriting

[New Blog Post] Bottom Up Egraph Ematching Plays Nicer with Theories (AC, etc) https://philipzucker.com/bottom_up/ #egraph #python #termrewriting

I had fun this weekend re-creating the examples from original congruence closure paper from 1980 in Python using egglog

https://egglog-python.readthedocs.io/latest/explanation/2023_12_02_congruence_closure.html

#egraph #formal_methods

I had fun this weekend re-creating the examples from original congruence closure paper from 1980 in Python using egglog

https://egglog-python.readthedocs.io/latest/explanation/2023_12_02_congruence_closure.html

#egraph #formal_methods

Can you name that algorithm based on this dataflow representation?

It's Linear Discriminant Analysis as implemented by Scikit Learn!

I finished up a notebook showing how you can build an Array API compatible library with the egglog e-graph library in Python and use that to optimize a #scikit-learn algorithm with #numba

https://egg-smol-python.readthedocs.io/en/stable/tutorials/sklearn.html

For more context, I gave a talk on the broader goals this summer:

https://egg-smol-python.readthedocs.io/en/stable/explanation/2023_07_presentation.html

https://www.youtube.com/watch?v=Pbi2uV9vWPg

#pydata #egraph #python

[New Blog Post] Answer Set Programming for E-Graph DAG Extraction #egraph #asp
https://www.philipzucker.com/asp-for-egraph-extraction/