philzook

7 ms·

31.
by philzook 2y ago
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
32.
Symbolic Execution by Overloading __bool__(philipzucker.com)
81 points by philzook 2y ago|10 comments
33.
Higher Order Pattern Unification on the Z3py AST(philipzucker.com)
2 points by philzook 2y ago|0 comments
34.
by philzook 2y ago
Beautiful stuff, great post!
35.
Tensors and Graphs: Canonization by Search(philipzucker.com)
1 points by philzook 2y ago|0 comments
36.
by philzook 2y ago
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
37.
Acyclic Egraphs and Smart Constructors(philipzucker.com)
4 points by philzook 2y ago|0 comments
38.
String Knuth Bendix(philipzucker.com)
2 points by philzook 2y ago|0 comments
39.
by philzook 2y ago
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 cert
40.
by philzook 2y ago
These are really interesting suggestions.
41.
by philzook 2y ago
It is as finished as it's going to be. I may write about the ordinals again, maybe I'll reuse pieces, but I won't be improving this particular page except with the occasional addendum.
42.
by philzook 2y ago
I leave my notes at the bottom of my posts. It is a combination link dump, half thoughts, speculation, parts I was too exhausted to flesh out. I recommend the technique. - It is actually the part that is the most valuable for me to refer to
43.
by philzook 2y ago
The main "software" application I'm aware of is a connection to termination checking (whether a program actually finishes). This is in turn connected to automated complexity analysis, which is a more refined answer about how
44.
by philzook 2y ago
No promises above Bits and Bobbles and definitely no promises below.
45.
by philzook 2y ago
Yea, I think it's a very neat structure. The typical presentation of the general concept of ordinals as an aspect of set theory hides a more down to earth cute algorithmic thing.
46.
Ordinals aren't much worse than Quaternions(philipzucker.com)
62 points by philzook 2y ago|28 comments
47.
by philzook 2y ago
I've got a related one I like. Why are the Avogadro's number and Boltzmann's constant inverses of each other N ~ 1/k? The statement doesn't make sense because the units don't work out, but it is true in mks. It
48.
by philzook 2y ago
I think you are not doing this line of work justice. Lattices like intervals or sets of values or zero/nonzero are typical and natural even without studying lots of theory. I believe this paper is about how you can use the concept of a
49.
by philzook 2y ago
Keep em coming! I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even
50.
by philzook 2y ago
Very interesting.
51.
by philzook 2y ago
That's a an interesting suggestion! By design, I can swap out or export to nanoCoP-i https://leancop.de/nanocop-i/ , an intuitionistic prover, but I haven't had a good theory the play with. I was considering
52.
by philzook 2y ago
This is a tough comparison. They are very similar in some respects but also very distinct. Prolog has some operational flavor to it. You can predict what it'll do. It can be used as "just" a programming language akin to pytho
53.
by philzook 2y ago
I think what you're referring to is code generation or extraction https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.... out of knuckledragger? It wouldn't be that difficult to travers
54.
by philzook 2y ago
Z3 is a marvel. Even if this project is of no interest to a person, Z3 might be. I have intentionally, literally, used z3 data structures to make that transition easier should one find something intriguing here over top of what z3 offers.
55.
by philzook 2y ago
Not naive. It is not trying to prove things about python code. It is building facilities and theory libraries around the pre-existing z3 python interface in a manner that can be reasonably called an interactive theorem prover. Hopefully, ev
56.
by philzook 2y ago
This is my windmill tilting project. Pretty raw off the bench kind of stuff, but I'm interested to hear what kinds of things people would use this kind of thing for or ways to make this more understandable to an audience not soaked in
57.
Knuckledragger, a Semi-Automated Python Proof Assistant(philipzucker.com)
71 points by philzook 2y ago|24 comments
58.
by philzook 2y ago
I am quite pleased with the ability to easily use prolog from within python and vice versa. It makes it now one of the easiest and most expressive solvers to plug into for my tastes. I'm starting to accumulate useful solvers here htt
59.
by philzook 2y ago
We found these ideas very useful for doing micropatches, post hoc intrafunction binary patches, using off the shelf compilers. At the least, a voice of support that these kinds of calling convention control is useful. - Copy and Micropatch
60.
Hashing Modulo Theories(philipzucker.com)
59 points by philzook 2y ago|3 comments

More ›