Does anyone know similar things ?

Turing 2016 tribute and the notorious SE chat ad / Tmachine blog

@vzn With respect to compression, straight-line programm representation of free algebras, variable substitution and cut-elimination in logic are all examples of compression, and it is easy to connect those to P vs NP. The principle is that a subexpression gets named by a variable, and that variable is subsequently used instead of the subexpression.

A similar mechanism (a subgeometry gets named by a cell, and that cell is subsequently used instead of the subgeometry) is also used for compressing semiconductor mask layouts. In this context, group theory is also allowed to play a minor part, because those cells can get shifted and rotated when referenced, and the references can also be arranged into an array. However, the additional compression allowed by group theory is only a fixed factor in this context, because no scaling is used

and the rotation angles are multiples of 45 degree.

@ThomasKlimpel yes that is the basic idea etc but on the other hand can you find a single major ref to P vs NP in terms of "compression" or "compressibility"? there is maybe some on kolmogorov complexity... (recall a paper by fortnow...) have long wondered if it might be a possible rosetta stone...

There are many refs for proof complexity, where Frege and extended Frege systems are compared, and extended Frege systems are basically the ones which allow for the sort of compression I described above (without the group theoretic extensions). I personally would still like to see more treatments using the straight-line represenation, because it occurs as one of the most natural forms of compression to me. For me, Kolmogorov complexity feels too artificial and non-commital.

@ThomasKlimpel have never gotten much into descriptive complexity but Cook himself has been hammering away at it for decades. yes some of relevant to P vs NP/ other classes etc but still think youre kinda missing my point, dont think they talk about "compression" much.

btw/ fyi reminded / thought of our old conversation(s) when Neumaier dropped by the last physics speaker chat session. he declined so far as guest speaker.

Indeed, Cook himself has done quite some work on proof complexity. However, proof complexity is quite different from descriptive complexity. For me as a logician, descriptive complexity feels a bit like cheating, why not be honest and call it finite model theory. Proof complexity on the other hand feels less like cheating to me, yes it is mostly only propositional proof complexity, but at least those are "true real world" symbolic logic deduction systems which are investigated.

@ThomasKlimpel afaik cook has worked on both proof/ descriptive complexity & think they are closely connected but not very up on either myself.

Well, one is plain symbolic logic, and the other one has a finiteness assumption. Since we know that logic cannot express such finiteness assumptions, it is hard to accept this as true logic.

But of course it depend on what gets described by descriptive complexity theory. If it is used to describe regular languages, then it naturally leads to finite state machines on infinite words, and it all makes sense even in the infinite case. So in this case descriptive complexity is fine for me, and is not cheating.

@ThomasKlimpel are you saying proof theory has the finiteness assumption?

No, descriptive complexity theory has the finiteness assumption.

@ThomasKlimpel sorry maybe only have a very cursory bkg in these areas & cant really comment much... but also doubt the distinctions you are making are all that meaningful

You know, anybody could have come up with the name "proof complexity", because it more or less adequately describes what is investigated. If you don't know what is meant by "descriptive complexity", you can't guess it just from the name. And if you would need to come up with a name for the field, it is much more probable that you name it "finite model theory", than that you name it "descriptive complexity". It is a marketing name!

@ThomasKlimpel lol think its useless to worry much about some math naming conventions, there are many examples of misnomers in the field... one could create a very large & amusing list... it would be fun if someone did that... as for mathematicians or scientists complaining about "advertising/ marketing/ promotion", more amusement by me there...

From my point of view, circuit complexity and proof complexity are two approaches with a real chance to make progress in complexity theory. Both approaches are somewhat related, and both have been made slow real progress over the years. But descriptive complexity on the other hand still holds the record for being misapplied in proposed proofs of open complexity theory conjectures.

@ThomasKlimpel dont think one cant really legitimately hold misapplications of a theory against the theory. aaronson is on record in his blog as disliking descr complexity (maybe with good reason), but its all kind of academic at times

some approaches do die out over time, there is definitely some fashion in mathematics... but its not so easy to figure that out/ see it in the moment...

am a big fan of circuit complexity too, but have you heard of "natural proofs"? its a nearly 2 decades old barrier that nobody seems to have the slightest idea how to overcome

Hasn't Mathias Hauptmann published a proof which is not affected by any of those barriers?

@ThomasKlimpel lol have you looked into it much? yeah noticed he did at least "address" natural proofs barrier. strangely, my blog on it is getting a smattering of hits, maybe real academics are starting to poke at it a bit...

I started reading the background material. It is interesting that there are two types of speedup theorems. The simpler type of speedup theorem just exploits the fact that Turing machines are mixing the algorithm and the hardware on which the algorithm is executed together into an inseparable mess.

am impressed with his bkg/ choice of citations, but havent dug into the rest much yet

The other type of speedup theorem uses diagonalization to construct recursive functions so complicated that there really isn't a fastest algorithm for evaluating them. In a way Hauptmann seems to have found a way around the inseparable mess, by working in a mode similar to the more complicated type of speedup theorem.

never did understand that speedup stuff that well. reminds me of blums speedup axiom. something like there exist languages with no optimal machine. never got exactly how they relate to constructible languages. always was kinda wondering about that stuff, had urge to ask expert(s)

@vzn Did Neumaier said anything interesting during the chat session?

@ThomasKlimpel think he asked sharp questions, dont recall the details, its in the transcript, we have to index/ link the transcripts sometime... yuggib the spker is a phd mathematician working on mathematical physics...

There was a meta post for the first chat session with links. Was yuggib the speaker of the second chat session? Or was it already the third session?

@ThomasKlimpel yuggib 2nd speaker. we havent linked the transcripts up to posts yet, wanna do that. 3rd spker upcoming, sank

Daniel Sank is impressive, he is from the Martini group, no?

@ThomasKlimpel right. martinis. am gonna write up a blog fairly soon. its amazing he was already a (physics) chat regular, so far the case with all the spkers, a bit surprised he agreed, it did take some wooing so to speak. have chatted with DS quite a bit over the months

Funny, I really learned a lot of physics in the last few month (mostly solid state physics), but I haven't followed what went on in the internet, physicsoverflow, or stackexchange about physics. Now I have at least some idea what is meant by chemical potential, Fermi level, Fermi surface, work function, debye model, drude model, band-structuture, dielectric function theory, drift diffusion equation, ...

@ThomasKlimpel yeah semiconductor fab is now/ long cutting edge physics. hey dont worry you prob didnt miss much :|

Well, then I will do a bit of logic now, so relaxing (and maybe I will finish it some day). Was nice chatting with you.

@ThomasKlimpel nice chatting take care man glad you still visit cyberspace sometimes, let me know if you figure/ hear anything re hauptmann etc