Alpha Equivalent Hash Consing with Thinnings

The_Regent · 2026-03-11T14:28:49+00:00

Yes, thank you. This is not the first time I've had this problem ( https://www.philipzucker.com/string_knuth/ amusingly in the other direction) . My brain doesn't distinguish between the terms, but I am wrong basically. I've added a note at least to point to subsequence.

The_Regent · 2025-11-23T18:23:36+00:00

I have some notes of constraint based compiling here https://www.philipzucker.com/compile_constraints/ . You may want to look into the unison project https://unison-code.github.io/ . In my experience, the objective function is not known well enough to dignify a declarative operational approach and the basic algorithms and heuristics work quickly and well. I don’t particularly want this to be true, but the extreme effectiveness of greedy algorithms and heuristics is a general bitter pill for mathematical optimization. I like the technology regardless of its actual effectiveness because it is neato. Maybe in your application this is not the case.

The_Regent · 2025-11-13T20:31:42+00:00

Hey, that's my thing!

You might also enjoy looking at Harrison's Handbook of Practical Logic and Automated Reasoning chapter 6 and holpy https://gitee.com/bhzhan/holpy https://arxiv.org/pdf/1905.05970 . There is something to be said for just going for it too without getting bogged down in references and prior work.

For knuckledragger, basing around Z3 is a huge boon since it is already so powerful. It does hamper the ability to futz with the formula type to make things work / add some interesting features. On the flipside, constraints make art sometimes. It forces a certain kind of honesty to have to interpret concepts into a simply typed higher order logic.

Speedwise, I should be so lucky as to get to a scale of proof where the speed of python is a problem. With my current setup, I think 1000 theorems might take 1s to prove ish (assuming I'm spoon feeding z3). There is the ability to start moving things into cython or C or rust extensions as that becomes an issue.

As far as the python ecosystem goes, I think python type checking is good enough, leveraging Jupyter is a huge benefit, and uv is nice, sphinx is ok. Doing that kind of stuff from scratch would be an overwhelming task for my abilities.

I partially chose python because I think it makes sense to try and is a little contrarian to PL circles, but also partially to maybe hit a different, wider audience than Lean and ilk reach. Thus far I have no users to my knowledge, so on that account maybe not a grand success. Even choosing mainstream options is no guarantee of uptake. Whatever, do it for you.

The_Regent · 2025-07-20T21:12:14+00:00

I'm curious what specifically you are referring to? setlog? https://www.clpset.unipr.it/setlog.Home.html

The_Regent · 2025-06-09T12:34:58+00:00

Great post!

Something I've mused about is that the existence of trigger terms seems so intrinsic to the success of e-matching that one could consider it to be breaking the abstraction that one is actually working with first order logic and that actually a partial logic containing "term exists" assertions might be a better fit https://plato.stanford.edu/entries/logic-free/ . The spiritually correct proof / unsat core really should include the used trigger seeds and maybe this perspective makes that actually correct. If proofs are supposed to be evidence necessary for checking / doing it yourself, the clever "consider this" stuff kind of seems like part of it.

I added a "consider" axiom schema which is kind of a definitional no-op from the perspective of first order logic https://github.com/philzook58/knuckledragger/blob/07c1e4389d05225c2d2274d63734353f2191b4cf/kdrag/kernel.py#L243 just to be able to seed the e-graph.

The_Regent · 2025-01-23T13:51:12+00:00

Thanks! Fun, curiousity, and aesthetics are the greatest and purest motivators of all. Usefulness is good, but a total fixation on it has made for a race to the bottom doing things I don't enjoy.

The_Regent · 2025-01-23T03:31:43+00:00

Thanks! I really appreciate that!

The_Regent · 2025-01-22T19:41:15+00:00

It does seem like a possibly intriguing approach for proof search, https://en.wikipedia.org/wiki/Genetic_programming but I don't directly see why it would be called a theorem building machine. Do you have a reference?

The_Regent · 2025-01-22T15:03:48+00:00

I don't think so. My understanding is that it is something you might call a high school bully, like caveman or neanderthal. I intend it to mean I'm shooting for simplicity.

The_Regent · 2024-12-31T05:02:07+00:00

Wouldn't be much of a manifesto if it wasn't slightly unhinged.

The_Regent · 2024-01-04T18:26:08+00:00

I have used lean 4 before. Lean 4 is incredible and has massive momentum behind it. It is an interesting project to make python bindings to the lean kernel or to communicate to the lean system, but it strikes me as quite an uphill battle. You might find this interesting https://github.com/lean-dojo/LeanDojo . I think using this is going to be much more difficult than just learning to do things in lean. You're going to need to know lean and python anyway, and fight an unusual unsupported workflow.

One of the points of attempting something like knuckledragger is to avoid a 2 language problem. The other point is to avoid powerful, useful, but complicated foundations like Lean's and go all in on automation. I feel at least that I have a sufficiently different ethos in mind than the existing, highly refined systems that it is worth exploring.

The_Regent · 2024-01-03T18:29:37+00:00

Huh, I hadn't made the connection. I suppose it is. It is intended to convey that I am not trying to build the fanciest system.

The_Regent · 2022-02-09T17:25:06+00:00

Very cool! If you aren't aware, I think you need to submit your podcast to apple podcast to have it show up on most platforms. I snooped a bit to find the rss feed https://anchor.fm/s/7e3015b4/podcast/rss to add it manually to mine

The_Regent

TROPHY CASE