> It's intended to understand the nature and theoretical limits of computation.
Not in a general sense, at least for standard complexity theory. It only deals with a very specific model of computation. Anyone with a sufficiently solid grasp of metamathematics intuitively understands that the distinction between solve and verify is nothing but a description of how badly matched our foundations are for the structure we're trying to view.
... This is the second time today I've posted about foundations like this.
>Not in a general sense, at least for standard complexity theory. It only deals with a very specific model of computation.
What is an example of a model of computation where complexity theory doesn't apply?
Standard complexity theory focuses on answering questions when our substrate behaves like a Turing machine with multiple tapes.
Consider it like this, if the answer is in our system's axioms, we don't have to do anything. In a trivial sense that means we're just given the answer table, but it's also true if our substrate matches the model of computation its simulating. IE for an SLD-Resolution machine, running an SLD-Resolution object language, unification is worst case O(1). This is a degenerate case of course, but it's an example of something that's not realizable on a Turing machine's semantics where the worst case is in... EXPTIME? It's not great.
The more we treat our substrate like building blocks, and less like a holistic oracle, that changes our complexity landscape. Complexity theory was never about studying that whole landscape.
You might want to say CT is pragmatic and focused on realizable machines. There are two problems with that:
1. There's nothing special with the baseline used for complexity theory other than its familiarity. Reality is our ultimate substrate. The universe is not Turing tape. There is absolutely no serious basis upon which an argument against substrates can be made, especially with how little we know and understand about the universe.
2. Complexity theory isn't so pragmatic to only study the finitely bounded, which also changes everything. There seems a very tight upper bound on information in the universe. Even studying up to it as a limit is decidedly not pragmatic in the slightest. This is perfectly fine of course, the problem only enters in when we want to be "pragmatic" on some things, but not others.
I also want to clarify: There are higher orders of complexity theory that have generalized a lot of its concepts, even into hypercomputation which is cool, but then there's another problem I didn't mention. Complexity theory still isn't about what he said. It quantifies that distance between prove and verify, but it doesn't study the set of all those distances and how they arise. It just quantifies them one at a time and has only a limited number of things to say beyond that. What he described is simply mathematical logic.
We actually understand quite a bit about the universe and the kinds of computers we can build. People also think about computers in speculative physics scenarios, eg closed timelike curves can be used to solve pspace complete problems.
I don’t think you can plausibly argue that complexity theory‘s base assumptions are a bad choice, at least not in the sense that you would assume that you can build exponentially more powerful computers in the physical universe. In fact, concerns about energy densities, limited amounts of matter, and the speed of light make it more difficult than typical machine models assume.
> Standard complexity theory focuses on answering questions when our substrate behaves like a Turing machine with multiple tapes.
This is not true. Complexity theory very much looks at complexity under different models (alphabet size, oracles, circuits). It's just that often (e.g. in the case of alphabets), there is a reduction of known complexity between two models.
> It quantifies that distance between prove and verify, but it doesn't study the set of all those distances and how they arise.
This is also not true (https://en.wikipedia.org/wiki/Proof_complexity).
> there is a reduction of known complexity between two models.
Every single time I've seen, for example, the lambda calculus be assigned cost semantics, it usually looks like what you would expect out of a Turing machine's simulation of it. Often times, they're explicit about it: https://www.sciencedirect.com/science/article/pii/S030439750...
For me, I can't accept that this is the criteria of "reasonable." Especially not for abstract theory.
I did try to indicate I'm mostly talking about standard complexity theory, the stuff you'd encounter on the surface level of the field. I'm not an expert in CT, but I do know enough to know what Landauer's principle is (and that it's been plausibly challenged.) I also know there's some crazy stuff in there, like descriptive complexity theory's link between Existential SOL and NP-Complexity.
> This is also not true (https://en.wikipedia.org/wiki/Proof_complexity).
Do you have any complexity theory papers that deal with this specifically? I've only ever seen that kind of work done in mathematical logic. Genuine interest in reading the CT approach.
> it usually looks like what you would expect out of a Turing machine's simulation of it
You could assign it any cost model you want. Often this doesn't make a difference (as speedup theorems and other "distracting details" mean that most classes are intended to be separated by exponentials), but it is true that people are typically more interested in cost models that are more relevant to the physical universe (although number of reductions is very much the cost of focus in proof complexity). Indeed, relevant discoveries in physics yield corresponding computational complexity research, as in the case of quantum complexity (https://en.wikipedia.org/wiki/Quantum_complexity_theory).
> Do you have any complexity theory papers that deal with this specifically?
A Google Scholar search for "proof complexity" will show you many papers as well as a number of books.
The point that what gets published adapts to the state of the art is fair. Personally I think its adaptations for ANNs and interaction nets are more interesting than the quantum ones. Once it has to account for the topology of the computer, or deal with non-atomic and continuous substrates, it changes a little bit. But this is orthogonal. The point wasn't that you can't make it adapt, I hope it doesn't come across like I'm dismissing the field and its importance. What I'm trying to say rather specifically is that it's not it's not about studying the nature of computation. It lives at a different level of theory than that. It might just be a disagreement on the article being used. I think it would be fair to say it studies a nature, just not the nature, but that would be true of all fields of CS.
I would say that it very much is about the nature of computation, but computation itself has always been tied to the physical. The physicality (even hypothetical physicality) is exactly what separates theoretical computer science from pure mathematics. Even the two primary resources that complexity measures - time and space - are tied to physical quantities.
The distinction is certainly a fair one to make. The etymological root of computation is "done with mental labor", by way of "to clean a financial ledger" (although weirdly, this isn't the real root. Putare is botancial pruning. Computare is a metaphor created after it spent some time on the semantic treadmill.) Grounding it to the physical is perfectly sane, because that's historically how it's been used.
That being said, a counterargument to press against this is that complexity theory doesn't restrict itself to physical or hypothetical physicality in its totality. As I mentioned, there are swaths of complexity theory work which bound quite far afield. The higher orders of the field are decidedly not-physical at all (and pedantically, hypercomputation isn't strictly computation). Of course even beyond this, we're still not studying the nature of computation, we're studying the cost. While you might say that of course these things are tied thanks to physicality (I wouldn't agree that they're equivalent on this basis, but I don't think that's an interesting semantic argument), I did also mention Landauer's principle being plausibly challenged, which is further problematic for conflating the two. Computation being reversible where entropy isn't doesn't explode complexity theory, but it does drive a wedge between information in a computer-sense and information in a thermodynamics sense. At that point, we don't have the claim in the first place, it's just a false friend. Something to consider.
I'm not saying computational complexity restricts itself to the physically realisable, I said it's tied to it and so there will be more papers on models that have some correspondence with physical reality.
> we're still not studying the nature of computation, we're studying the cost
That is one way of studying the nature of things, sort of like the use of the Hamiltonian in physics, especially if you're interested in problems and classes of problems, and their broad similarities and differences via reductions, rather than in specific computations.
> The higher orders of the field are decidedly not-physical at all (and pedantically, hypercomputation isn't strictly computation).
Hypercomputation isn't really a big part of the main thrust of complexity theory, but (computable) oracles do very much play an important role in complexity theory, even in its lowest complexity classes, such as in the relativisation barrier, which shows that some proof techniques cannot separate P from NP.
> I did also mention Landauer's principle being plausibly challenged,
That's not complexity theory, at least not the standard theory, which treats time and space (or circuit size) more abstractly than concrete physics. There are, however, theoretical reversible models, just note that they don't yield different "classic" deterministic complexity classes (i.e. they do not yield exponential differences).
Again, all fair. To simplify, my points are to demonstrate a confounding nuance, simple counterexamples where the arguments don't hold.
> Hypercomputation isn't really a big part of the main thrust of complexity theory
I don't mean to imply that it was, though the results are actually relatively important elsewhere.
> That's not complexity theory, at least not the standard theory, which treats time and space (or circuit size) more abstractly than concrete physics.
More, but not totally abstractly. Steps and cells being vacuous primitives, they're not literally space-time, but within orthodoxy there's absolutely a partial morphism that's implied. That's why they're named like that. You are supposed to have them live close together in your head.
>There are, however, theoretical reversible models, just note that they don't yield different "classic" complexity classes
I know that some don't, but for example quantum models to use your own example, while not technically reversible in the absolute sense, do possess some reversibility capability and do derive different complexity classes.
I think it's very obvious that there should be reversible computational models which yield different complexity classes from the typical ones. To me for a field to qualify as a study on the nature of computation, it should probably be able to design one totally a posteriori, if in a higher order language. Complexity theory might be invoked in such a construction, but it's not the one doing the building. It's one of many in an orchestra.
Here's a question I have, since you do seem pretty well versed on CT. Universal quantification over complexity classes of first-order systems, used anywhere in the abstract?
> Universal quantification over complexity classes of first-order systems, used anywhere in the abstract?
I'm not sure what you mean by "complexity classes of first-order systems" and by "in the abstract".
But it seems like you're asking about the intersection of computational complexity and formal systems, and there's definitely work there. I already mentioned proof complexity, which analyses the number of deduction steps needed to prove something in various formalisms, and there are famous undergrad-level examples, such as TQBF (https://en.wikipedia.org/wiki/True_quantified_Boolean_formul...). But an intersection that is of more interest to me, as I'm interested in software correctness, is that of the model-checking problem.
Now, many people are confused whenever the model checking problem is discussed, because they confuse it with model checkers, which are a set of algorithms intended to solve the problem, but complexity theory is typically interested in the inherent difficulty of answering problems regardless of the algorithm used to do it. So the model checking problem is that of determining whether a formula in some formalism implies another formula, and its inherent complexity exists regardless of whether this question is answered via a formal proof or by some technique involving the logic's semantics. In the context of software verification, the model checking problem is that of determining - by whatever means - whether a program satisfies some non-trivial property.
Philippe Schnoebelen has some papers on the model checking problem in temporal logic (https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/Sch-aiml02..., https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/DLS-jcss-p...). One of his findings that I've found most interesting with regards to programming is that programming languages cannot, in general, make answering the question of whether a program satisfies some property any easier. This result is surprising. The reason is that without a programming language, we could describe a program as a huge state transition graph (this is called a Kripke structure). In that representation, it's been proven that verification is linear in the number of states, i.e. there is no general approach that is faster than brute-force. Now, the size relationship between a program written in a programming language and its Kripke structure is easily exponential or more, so if there were no algorithm that's better, in the worst case, than a brute force of the Kripke structure, then obviously verification is intractable in the size of the program. However, the number of Kripke structures of size N that have a succinct representation in some programming language is far smaller than the total number of Kripke structures of size N. So it could have been the case that analysing programs would have been easier than analysing their Kripke structure (while ignoring their representation in the language). But Schnoebelen proved that this is not the case.
He also proves that program decomposition (and verification of each component separately) cannot, in general, make verification any easier (i.e. the model checking problem isn't FPT in the number of program components).
These results are far more recent than the hopes expressed in the seventies and eighties that we'll be able to prove the correctness of all/most/many programs we write, and indeed, even though the results talk about the worst case, what we've seen in the last few decades is that the power of program verification indeed behaves more like the worst case than something far from it. The gap between the size of programs we can verify and the average size of programs we write has only widened (what saved the day has been the effectiveness of unsound methods, but that's a whole other discussion).
Isn't complexity theory usual based on a random-access model, not any kind of Turing machine?
MT Turing machines aren't really all that different. Or from pointer machines for that matter. They map nicely together.