philzook

I personally have a great respect and love of the intuitive and consider formalism or abstract mathematics only interesting in the service of elaboration or exploration of the intuitive.

Basically all optimizing compilers have a simplifier or rewriter in them. I don't see it as a requirement or even necessarily a priori desirable to frame their discussion or formulation in terms of high barrier mathematical language. Do so if it is fun or useful. Sometimes it is. It is to my subjective taste to do so. Compiler writers are a pretty clever group by and large and are aware of a decent amount of useful math.

There is also a tendency to underestimate where 10 years of study and effort applied to a subject can bring you and attribute it totally to some intrinsic intelligence.

Term rewriting _is_ really neat. Realizing and remembering what you find neat and exciting is important. I like equations.

Yes, perhaps. This is not written as a general introduction to e-graphs. They are a data structure that compactly holds many equivalent versions of terms / syntax trees. Egraphs are a solution to phase ordering issues for greedy rewrites. They are also just a useful fabric for optimization tasks. They are being used in many compiler projects https://github.com/philzook58/awesome-egraphs . Mostly research compilers, but cranelift and luminal are not for example.

Many applications are naturally expressed using bound variables (lambdas, summation expressions, einstein indices, integrals, loops) but the basic e-graph doesn't really support the concept. One can instead model using combinators (SKI combinators, relation algebra, categorical combinators, other) but this tends to be not entirely natural and tends to explodes in the search space of different ways to encode the same concept using combinators.

Lifting e-graphs are a variant of sorts of slotted e-graphs, which are techniques to supports binders in egraphs. It's more subtle to do so than one might think. Lambda microegg also adds a surface syntax to play around more easily.

A suggestion: I think the python api could be more useful if it returned a structured tree and possibly also could accept a structured tree. I'm guessing you're using maturin, there are some nice low energy ways of getting a tree like structure out even if you have to copy internal trees into a new version with nice python bindings. I've done similar things here https://github.com/philzook58/scryerpy https://github.com/philzook58/steelpy https://github.com/philzook58/microeggpy

It's a really neat board. You can get kits from aliexpress etc. I wrote up some notes here https://www.philipzucker.com/td4-4bit-cpu/ . English descriptions are not so readily available.

I also had some fun modelling the chips in verilog and model checking a verilog interpreter against them. https://www.philipzucker.com/td4_ebmc/ George Rennie got a similar thing working using the yosys toolchain https://github.com/georgerennie/philip_zucker_sby_demo

Interesting. I think there is even more similarity if you are trying to find a "best" list from which two other lists are thinned.

https://www.philipzucker.com/ I blog regularly about egraphs, SMT solvers, assembly verification, theorem proving

I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/

I'm working on Knuckledragger, a proof assistant shallowly based upon z3py https://github.com/philzook58/knuckledragger

Yesterday I proved the infinitude of primes, which I was pretty happy with. https://www.philipzucker.com/knuckle_primes/ A trivial theorem in the scheme of things, but one for which z3 certainly can't do it on it's own.

Yeah, using `<=` in this way is pretty sinful.

My maybe inaccurate understanding of recursive CTEs was that they only allow linear occurrences of the recursively defined relation in the query and do not allow many mutually recursively defined relations. These might be per implementation restrictions. These are pretty harsh restrictions from a datalog perspective. I should explore what Postgres offers more. It's just so easy to try stuff out on sqlite.

My suspicion is that if you can get away with it that recursive CTEs would be more performant than doing the datalog iteration query by query. AFAIK for general rules the latter is the only option though. I had a scam in that post to do seminaive using timestamps but it was ugly. I recently came across this new feature in duckdb and was wondering if there is some way to use it to make a nice datalog https://duckdb.org/2025/05/23/using-key.html . Anything that adds expressiveness to recursive CTEs is a possibility in that direction

Love it! I was trying to use python as a dsl frontend to Z3 in a different way https://github.com/philzook58/knuckledragger/blob/ecac7a568a... (it probably has to be done syntactically rather than by overloading in order to make `if` `and` etc work). Still not sure if it is ultimately a good idea. I think it's really neat how you're abusing `,` and `:` in these examples

Thanks! I wouldn't so much say it was written so much as it was vomited out in a year of enthusiasm, but I'm glad it has some value.

Nice!

I'll note there is a really shallow version of naive datalog I rather like if you're willing to compromise on syntax and nonlinear variable use.

   edge = {(1,2), (2,3)}
   path = set()
   for i in range(10):
       # path(x,y) :- edge(x,y).
       path |= edge
       # path(x,z) :- edge(x,y), path(y,z).
       path |= {(x,z) for x,y in edge for (y1,z) in path if y == y1}

Similarly it's pretty easy to hand write SQL in a style that looks similar and gain a lot of functionality and performance from stock database engines. https://www.philipzucker.com/tiny-sqlite-datalog/

I wrote a small datalog from the Z3 AST to sqlite recently along these lines https://github.com/philzook58/knuckledragger/blob/main/kdrag...

What is the distinction between this approach and Address Sanitizer https://clang.llvm.org/docs/AddressSanitizer.html ? If I understand correctly, Fil-C is a modified version of LLVM. Is your metadata more lightweight, catches more bugs? Could it become a pass in regular LLVM?

Wide context.

But to be a bit more specific, I've been involved in the egraphs community https://github.com/philzook58/awesome-egraphs and we don't currently have a shared database of rewrite rules for benchmarking, nor do we collect the rules from different projects. Seeing the actual files is helpful.

On a slightly different front, I'm also trying to collect rules or interesting theories up in my python interactive theorem prover Knuckledragger https://github.com/philzook58/knuckledragger . Rewrite rule or equational theory looking things are easier to work with than things with deeply nested notions of quantifiers or tons of typeclass / mathematical abstraction like you find when you try to translate out of Coq, Lean, Isabelle.

There are also different approaches to declarative rewrite rules in major compilers. GCC, LLVM, and cranelift have their own declarative rewrite rule systems for describing instruction selection and peephole optimizations but also of course lots of code that programatically does this. I also want to collate these sorts of things. Working on fun clean systems while not confronting the ugly realities of the real and useful world is ultimately empty feeling. Science is about observing and systematizing. Computer science ought to include occasionally observing what people actually do or need.

This looks great! Are there files or sections in particular I might want to focus on?

Surely Hacker News has awareness of many, many rewrite rule files. Keep em coming!

I don't always care about consistency between rule sets. Depends what I'm trying to do.

The question at hand is motivating and getting benchmarks for different approaches or engines to equational reasoning / rewriting. I sometimes lose sight of motivations and get discouraged. Doing associativity and commutativity and constant fusion for the nth time I start to become worried it's all useless.

I'm curious if there is a useful connection between Apache's rule and other term rewriting. Some sort of static analysis? If there is a interesting database of them, I'd add it.

Just celebrated my 10 year anniversary https://www.philipzucker.com/ten_year_blog/ actually. It has not generated new jobs for me, but I haven't been looking really. Writing is good. It's a good way to learn more. It's good to do things and have tangible results. If you don't enjoy it on some level or feel satisfaction, there are more direct ways to seek what you want.

It's interesting how sometimes it feels like a topic starts showing up super often all of the sudden. It probably isn't a coincidence, since my interest and probably this post's interest is due to Tao's recent equation challenge https://teorth.github.io/equational_theories/ .

I was surprised and intrigued to find Wolfram's name when I was reading background literature doing this blog post https://www.philipzucker.com/cody_sheffer/ where I translated my friend's Lean proof of the correspondence of Sheffer stroke to Boolean algebra in my python proof assistant knuckledragger https://github.com/philzook58/knuckledragger (an easier result than Wolfram's single axiom one).

I was also intrigued reading about the equational theorem prover Waldmeister https://www.mpi-inf.mpg.de/departments/automation-of-logic/s... that it may have been acquired by Mathematica? It's hard to know how Mathematica's equational reasoning system is powered behind the scenes.

Mathematica can really make for some stunning visuals. Quite impressive.

Thank you, this is fascinating advice

https://github.com/domschrei/mallob I've seen talks by AWS where they claim that distributed SAT solving is very effective.

Do you need it to be parallel or just fast? My impression is that at the single machine level, it's hard to beat kissat and the CPU or GPU parallelism is not that useful. https://github.com/arminbiere/kissat

It's a good question. I was asking something like this myself at lunch today.

Basically I think the issue is that SAT solvers accept stuff at a conjunctive normal form level, which is pretty far from what you'd want to use for most applications. It's more like an IR. So SAT solvers are more typically backends to higher level tools which compile to them.

If your tool offers a high level interface, one may be inclined to just call it an SMT solver. I too despite being interested in SAT, basically reach for an SMT solver even if my problem is pure boolean because of convenience.

- SAT/SMT by example is an excellent text https://smt.st/

- https://pysathq.github.io/ offers a nicer interface directly to SAT solvers

- Z3 https://microsoft.github.io/z3guide/docs/logic/intro/ can put problems into CNF and pretty print dimacs. It contains a SAT solver, but one would probably expect a purely boolean problem to do better on the top of the line SAT-only solver like Kissat.

I am also a bit surprised, but happy that people find value here. Maybe just pretend the article ends before "bits and bobbles". Then it is just a short note on a brute force solver and a Davis Putnam solver. I like keeping my notes in my posts because it's useful for me to do so and helps psychologically with editing and scope creep. People have been able to interpret what I was getting at but didn't flesh out a lot more than I expect. Sometimes they explain a point that I mention I was confused on or wondering about in the notes section.

This looks like a nice reflection of python into a syntax tree, but unless I'm mistaken, it can't reflect python control structures like if-then-else? Z3 or sympy already are kind of ready to go systems that overload all the typical operators. Is there something you've done here they are missing?

This looks great! The paper linked in your README https://hoheinzollern.files.wordpress.com/2008/04/seer1.pdf also seems like a nice explanation of similar ideas.

The reason I'm exploring this idea is to use more natural looking python as dsl for function definitions in my proof assistant https://github.com/philzook58/knuckledragger

Also to see if I can make a nice-looking staged metaprogramming framework in python like buildit, but maybe to generate C/C++ rather than more python.

Could Crosshair be used in these ways?

Beautiful stuff, great post!

I like what I find clearest (a moving target for all sorts of reasons). I typically find recursion clearest for things dealing with terms/ASTs. My coding style usually leans towards comprehensions or fold/map etc rather than loops. That's why I find the loop being clearer for this algorithm surprising.

How do you go from these definitions of ordinal arithmetic by transfinite recursion to mechanical rules for arithmetic on the cantor normal form / deriving the needed algebraic identities? It seems very non obvious to me, although certainly must be very obvious to many. I would like a reference if you have one.

I think a deficiency of my post is that I didn't go into much of what the ordinals are, but I think a strength is that it is all quite mechanical.