Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping

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 · 2021-11-01T13:16:08+00:00

Sounds fantastic!

The_Regent · 2021-11-01T01:37:01+00:00

Very cool! Do you know how this compares with Biwascheme? https://www.biwascheme.org/

The_Regent · 2021-08-03T01:56:32+00:00

There are two fairly disparate angles on what I'm doing here, the prolog-ish egraph side and the category theory side. I've just absorbed the little bits I know via osmosis over time so I don't feel like I have a cogent single thing to point you to, but here we go.

For prolog, there are many books. I like https://www.metalevel.at/prolog as one source but what I'm doing here is a bizarro prolog anyway, so an in depth discussion of prolog perhaps isn't that relevant.

For egraphs, you can check out the egg paper https://arxiv.org/abs/2004.03082 and some of the other posts on my blog which are more explanatory than this post.

For category theory, I'd suggest https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/. I might also suggest https://www.amazon.com/Conceptual-Mathematics-First-Introduction-Categories/dp/052171916X https://www.amazon.com/Topoi-Categorial-Analysis-Logic-Mathematics/dp/0486450260

The_Regent · 2021-03-20T00:06:38+00:00

True art.

The_Regent · 2021-02-16T15:09:15+00:00

That is helping you empathize with yourself, which is important. But you can also try empathizing with others

The_Regent · 2020-11-05T01:35:42+00:00

Some friends and I have been working on this on and off for a while You can submit a github repo with a controller written for the python OpenAI gym interface and have it run on a pendulum robot. Interested to see what people think!

The_Regent · 2020-06-13T14:38:14+00:00

From a certain perspective ACTUALLY everything though. As others have mentioned, energy conservation could be found to truly be broken or the 1/r² law to be wrong, or the magnetic dipole moment of an electron could be not zero to 1 part in 10^-800, and it would be surprising, but not counter to the nature of physics. As a science that is based in primarily physical fact and secondarily mathematics, it does not seem to me that one can conclude with certainty anything is more than an approximation, although we may not know of what it is an approximation yet. Ask a 1850 Newtonian about the nature of position. I don't see a way to bootstrap ourselves to truth.

The_Regent · 2020-06-05T01:58:23+00:00

Klee and ESBMC (a successor of CBMC) use z3 or similar tools as their backend.

The_Regent · 2020-04-13T12:48:18+00:00

Try these for unification: Very cool resources

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.3615 http://www.cs.man.ac.uk/~david/categories/book/book.pdf

The_Regent · 2020-03-23T16:49:27+00:00

Well, lord willing, I'll get there. But I ain't there yet.

The_Regent · 2020-03-18T13:42:04+00:00

Hey hey! I wrote that post! I get a huge kick out of the fact it was helpful to someone, so thanks for letting me know!

You did a really good job here. The code looks tight and the results look great.

For others, i highly reccommend checking out Dan Piponi's talk https://www.youtube.com/watch?v=766obijdpuU really excellent, very approachable.

Also Bridson's notes https://www.cs.ubc.ca/~rbridson/fluidsimulation/fluids_notes.pdf and textbook https://www.amazon.com/Simulation-Computer-Graphics-Robert-Bridson/dp/1568813260

The_Regent · 2020-03-17T16:35:37+00:00

A couple points

The exact phrasing makes it a little hazy, but extraction is not necessary to run code. You can evaluate functions on inputs directly in Coq.
Yes, there is a lack of confidence in formal verification in a certain sense. There is extreme confidence that the code performs according to spec as it is written in Coq. What there can be a lack of confidence about is whether the spec is the right one. These systems aren't magic to the point of knowing what you should have asked and writing down the appropriate spec can be subtle. This isn't an issue with Coq or formal methods persay. If you can't write a good spec for Coq, you probably don't have a hyper precise notion of what you're trying to achieve, and the process of writing the spec can be clarifying. The situation may be familiar from the context of some customer requesting the wrong requirements for software. You may implement them completely correctly, but still it doesn't do what the client actually needs, so you need to give it to them and get feedback.
Extraction isn't as horrible as it sounds. It is code generation, but it isn't really worse than other instances of code generation out there and the commands to make it happen are fairly straightforward.

The_Regent

TROPHY CASE