Philip Zucker[New Blog Post] Lifting and Lowering Functions with The Dump Calculus https://www.philipzucker.com/dump_calculus/ #python #functionalprogramming #logic #egraphs
Thinning/Lifting E-Graphs for Alpha Equivalence: Checkpoint I https://www.philipzucker.com/thin_egraph/ #rust #egraphs
Thinning/Lifting E-Graphs for Alpha Equivalence: Checkpoint I
Thinnings are something that shows up when you think about binders and contexts. I’ve been trying to build an alpha equivalence aware e-graph using the concept. For a moment complexity seemed spiralling out of control, but actually as I understand what is going on, I’m throwing out more and more code and things are getting simpler. I am overdue for checkpoint.
I put a new preprint up summarizing a year or so of fun e-graph ideas. Check it out! #egraphs #logic #compilers https://arxiv.org/abs/2504.14340
Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching
E-graphs are a data structure for equational reasoning and optimization over ground terms. One of the benefits of e-graph rewriting is that it can declaratively handle useful but difficult to orient identities like associativity and commutativity (AC) in a generic way. However, using these generic mechanisms is more computationally expensive than using bespoke routines on terms containing sets, multi-sets, linear expressions, polynomials, and binders. A natural question arises: How can one combine the generic capabilities of e-graph rewriting with these specialized theories. This paper discusses a pragmatic approach to this e-graphs modulo theories (EMT) question using two key ideas: bottom-up e-matching and semantic e-ids.
N-gated Hacker NewsSinons Blog presents "Efficient E-Matching for Super Optimizers," a groundbreaking revelation that computers can now tell when different-looking things are actually the same! 🤯 Who knew computers could be just as confused by appearances as humans? But fear not, #EGraphs and congruence closures are here to save the day by magically making things equal. 🪄✨
https://blog.vortan.dev/ematching/ #EfficientEMatching #SuperOptimizers #Technology #Innovation #ComputerScience #HackerNews #ngated
https://blog.vortan.dev/ematching/ #EfficientEMatching #SuperOptimizers #Technology #Innovation #ComputerScience #HackerNews #ngated
Hacker NewsSpecializing Python with E-Graphs
https://vectorfold.studio/blog/egglog
#HackerNews #Specializing #Python #with #E-Graphs #EGraphs #Python #Programming #Tech #News #HackerNews
[New Blog Post] An External Z3 Egraph for Egraphs Modulo Theories #egraphs #logic #smt https://www.philipzucker.com/ext_z3_egraph/
[New Blog Post] EGraphs as Ground Completion Talk and EGRAPHS 2024 notes https://philipzucker.com/egraph2024_talk_done/
@pldi #egraphs
@pldi #egraphs
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.