philzook
Joined 9 years ago
Karma
955
Submissions
302
Member since
Sep 19
Website: https://www.philipzucker.com
Twitter: https://twitter.com/SandMouth
View on Hacker NewsRecent submissions
Comment · 1 month ago
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.
Comment · 1 month ago
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.
Comment · 2 months ago
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
Comment · 5 months ago
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
Comment · 7 months ago
Interesting. I think there is even more similarity if you are trying to find a "best" list from which two other lists are thinned.
Comment · 9 months ago
https://www.philipzucker.com/ I blog regularly about egraphs, SMT solvers, assembly verification, theorem proving
Comment · 11 months ago
I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/
Comment · 1 year ago
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.
Comment · 1 year ago
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.
Comment · 1 year ago
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