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.
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.
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/
If I ever get around to writing my own at least somewhat serious Datalog engine, I definitely want to add a "translate to SQL" capability. Your work looks like the perfect inspiration, thanks!
(Also added a link to your article on what you can do with Datalog, excellent stuff, couldn't have written it better myself)
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
In some parallel world, Python is the perfect tool for language-oriented programming. Any decorated function is compiled by its own DSL compiler into the internal representation of the corresponding solver, and functions communicate with each other using rich Python data structures :)
Thank you! I have been searching for something like this but for some reason couldn't find your work.
I am currently implementing a Datalog to PostgreSQL query engine at work as we want to experiment with modeling authorization rules in Datalog and then run authorization queries directly in the database. As I want to minimize the round trips to the database I use a different approach than yours and translate Datalog programs to recursive CTEs. These are a bit limited, so we have to restrict ourselves to linearly recursive Datalog programs, but for the purpose of modeling authorization rules that seems to be enough (e.g. you can still model things such as "permissions propagate from groups to group members").
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
Yes, I think so too, if not just for the reduced number of round-trips to the database. The evaluation strategy that PostgreSQL employs for CTEs is essentially a degenerate form of seminaive evaluation where it only has to consider the delta for one subgoal in each rule due to being restricted to linearly recursive programs with no mutual recursion. The restriction to not have mutual recursion means that PostgreSQL can just stratify the CTE and compute a fixed point using the degenerate seminaive algorithm for each strata. Once a stratum is done, it can consider its idb as ground facts in the next, and so on.
I am really unhappy about the design of CTEs, and frankly I think it is a clunky hack designed by someone who was not aware of all the research on Datalog evaluation, which Ullman and others had already written excellent textbooks about at the time. CTEs are simultaneously too powerful - Turing-completeness in a declarative query language is a sure way to tell that the designers screwed up - and too restricted because being stuck in the Turing tarpit rules out so many techniques for optimization.
I didn't know about DuckDB's approach, but it seems to be a way to mark your relations as moded and exploit that during the evaluation. It appears to improve performance, but unfortunately the design it builds on is inherently flawed. I wish SQL would get a proper pure Datalog fragment in the future.
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?
For example, asan will totally let you access out of bounds of an object. Say buf[index] is an out-of-bounds access that ends up inside of another object. Asan will allow that. Fil-C won't. That's kind of a key spacial safety protection.
Asan is for finding bugs, at best. Fil-C is for actually making your code memory safe.
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.
Thanks for the explanation, although I now have more questions :
- Why the "graph" aspect of "e-graphs", when it seems all of the ones I've seen in your article and on Wikipedia have only a single edge? Why not just "equivalences"?
- The Wikipedia page doesn't seem to explain the actual data structure. If it's a data structure, how is the actual data laid out in a series of bits? Or is "data structure" on that page used in a way which is meant to make sense to mathematicians rather than computer scientists?
- How does this relate to existing refactoring tools? Is this a new approach? Or is it what IDEs and language servers already use?
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.
Fair enough. My personal motivation is abstraction logic (AL), and one way of viewing it is as a generalisation of equational reasoning. I am just starting to implement rewriting for AL, but I will definitely drop you a line once you can play around with it. Maybe AL can be your common format, instead of just a 15th engine for it :-) There are two reasons why I think that:
1. AL is more general than first-order rewriting, because it has general binders, that is general variable binding constructs.
2. Unlike higher-order logic, which also has general binders, it doesn't have types, so rewrite rules in AL can be taken for face value, and have no hidden type annotations in them, just like in first-order rewriting (that is a consequence of AL having a single mathematical universe).
I must admit, I am quite excited about implementing rewriting for AL! My PhD father has co-authored a book about (mostly) first-order term rewriting [1]. Higher-order rewriting based on the lambda calculus is mentioned briefly in it (and of course implemented in Isabelle), and I am wondering if rewriting based on AL instead will bring new insights and/or techniques.
reply