4 ms·

> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops f

> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever. Fair for many applications. I work with computers that write proofs. > Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But there's another issue here as well: we don't know whether P=NP. There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. > How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Well, not me! Formal methods and program synthesis are alive and well, but it's important to researchers in these areas to understand what parts of our work are decidable and what aren't. I should mention that Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, and tailoring tools to real user patterns can really blunt the problem of undecidability in practical use cases.

wizeman 4y ago
> There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. I mentioned this in another comment: isn't EXPTIME only defined for Turing machines? Which again, just touches on all of my points. For all we know, if you've reached the conclusion that an algorithm's complexity is EXPTIME, this conclusion could be just as false as the Halting problem and Rice's theorem are for real-world computers. > Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, My point is that you shouldn't believe that the theories are undecidable because those analysis were done using Turing machines as models. And the other point is that sure, there are many people doing formal methods, etc. But how many more would there be if most people believed the problem to be solvable?
- markusde 4y ago
  I think I see what you're getting at. A few final points: - There's a subtle difference between "infinite" and "unbounded". Turing machines use at most a finite amount of memory after any finite amount of steps (the tape always ends in an infinite sequence of empty cells), so a machine which starts with one cell and allocates one new cell every step is equivalent to a TM. - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. No stronger method of computation which can also be physically implemented is known to exist. edit: typo
  - wizeman 4y ago
    > - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me. So I'm not 100% sure that those measures of complexity have the same real-world meaning, for similar reasons. > - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. Yes, but even in that case, the amount of memory would be finite. Because the universe is expanding faster than the speed of light, there's only a finite amount of energy that is accessible at any point of spacetime (as far as I understand). So even in theory you can't say the amount of memory can scale infinitely (not to mention in practice). > - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. The theories are undecidable only if you assume a model of computation with infinite memory. Which can be interesting from the mathematical point of view, but not for applying those results to real-world problems, because now you've made a grave mistake: you believe something is undecidable when it is in fact decidable. I mean, sure, I can also invent a new super-duper-amazing model of computation that is even more powerful than Turing machines and can perform incredible Oracle-like feats and, say, run all programs in constant-time (yeah!), but it would not be correct to say that all the results obtained in this model apply to the real world. If an SMT solver is trying to prove that my program has a bug, even though some theory says that the problem is undecidable if my program was running on a theoretical Turing machine, this is meaningless to me (and quite misleading) because the problem is actually decidable given that my program is going to run on a computer. > No stronger method of computation which can also be physically implemented is known to exist. You say that like Turing machines can be physically implemented.
    - crdrost 4y ago
      Caveat, the thing that makes it decidable is not the fact that it was going to run on a computer with finite memory, the SMT solver will fail on many code chunks that can run on your computer. (And that's more or less the claim of the halting theorem, not that nothing useful can be done, but that anything done can only be heuristic.) What made it decidable was rather the fact that you did not use all of the power that your programming language makes available to you, you did not steer the program last the bounds where the heuristics work. This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language. The thing you immediately notice is a type error, “does the analyzer halt when given itself as an input?”... well, it doesn't know what to do, it was expecting an argument of type `ParseTree x` for some x and you handed it an argument of type `∀x. ParseTree x → Bool`... To get around this and build the liar paradox which makes the proof “go,” is not too hard: but you are basically forced to produce a quine instead and those techniques are non-trivial. In our normal programming lives, you could apply a heuristic that assumes we never do such things, and life is good. The focus on finite versus infinite memory is a huge distraction. If your halting detector applied to the above quine tried to not be a heuristic by salvaging the case where it runs out of memory while analyzing, you would get the result “this program will OOM, but if you run me in a machine with 1 meg less memory I will stop an odd number of cycles earlier and the program will not OOM, but will instead halt successfully telling you that the next cycle would OOM.” Suddenly your tests that you build with this thing are all flaky, because it didn't have the humility to be a heuristic and say “I don't know this is too complex for me,” and in the real world you are running on Linux and you don't know how many megs you really have available. Better just to not play any of that game. So yeah the problem with Turing machines is not that they have infinite memory, infinite memory is in fact a standard assumption that most programmers in GCed languages make when programming most of their programs. This is why “your problem isn't the garbage collector, it's that you're swimming in garbage” and all that. Put another way, Turing machines suck even if you enhance them to have 5 parallel tapes (God why do they not have parallel tapes by default, should have at least one for output, one for main memory, one for a stack, and some more as scratchpads) of bytes (seriously why are they still not bytes in textbooks) and enforce that the tapes each only have 1 billion symbols and any attempt to go off the edge crashes the Turing machine. You are joyous because it now only has finite memory, I can run a cycle detection with 10^{1 billion} nodes in the graph or whatever, so cycle detection is in principle solved! If you are as pragmatic as you say you are, you see that this is no help, halting is still effectively impossible.

wizeman 4y ago

> There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. I mentioned this in another comment: isn't EXPTIME only defined for Turing machines? Which again, just touches on all of my points. For all we know, if you've reached the conclusion that an algorithm's complexity is EXPTIME, this conclusion could be just as false as the Halting problem and Rice's theorem are for real-world computers. > Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, My point is that you shouldn't believe that the theories are undecidable because those analysis were done using Turing machines as models. And the other point is that sure, there are many people doing formal methods, etc. But how many more would there be if most people believed the problem to be solvable?

markusde 4y ago
I think I see what you're getting at. A few final points: - There's a subtle difference between "infinite" and "unbounded". Turing machines use at most a finite amount of memory after any finite amount of steps (the tape always ends in an infinite sequence of empty cells), so a machine which starts with one cell and allocates one new cell every step is equivalent to a TM. - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. No stronger method of computation which can also be physically implemented is known to exist. edit: typo
- wizeman 4y ago
  > - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me. So I'm not 100% sure that those measures of complexity have the same real-world meaning, for similar reasons. > - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. Yes, but even in that case, the amount of memory would be finite. Because the universe is expanding faster than the speed of light, there's only a finite amount of energy that is accessible at any point of spacetime (as far as I understand). So even in theory you can't say the amount of memory can scale infinitely (not to mention in practice). > - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. The theories are undecidable only if you assume a model of computation with infinite memory. Which can be interesting from the mathematical point of view, but not for applying those results to real-world problems, because now you've made a grave mistake: you believe something is undecidable when it is in fact decidable. I mean, sure, I can also invent a new super-duper-amazing model of computation that is even more powerful than Turing machines and can perform incredible Oracle-like feats and, say, run all programs in constant-time (yeah!), but it would not be correct to say that all the results obtained in this model apply to the real world. If an SMT solver is trying to prove that my program has a bug, even though some theory says that the problem is undecidable if my program was running on a theoretical Turing machine, this is meaningless to me (and quite misleading) because the problem is actually decidable given that my program is going to run on a computer. > No stronger method of computation which can also be physically implemented is known to exist. You say that like Turing machines can be physically implemented.
  - crdrost 4y ago
    Caveat, the thing that makes it decidable is not the fact that it was going to run on a computer with finite memory, the SMT solver will fail on many code chunks that can run on your computer. (And that's more or less the claim of the halting theorem, not that nothing useful can be done, but that anything done can only be heuristic.) What made it decidable was rather the fact that you did not use all of the power that your programming language makes available to you, you did not steer the program last the bounds where the heuristics work. This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language. The thing you immediately notice is a type error, “does the analyzer halt when given itself as an input?”... well, it doesn't know what to do, it was expecting an argument of type `ParseTree x` for some x and you handed it an argument of type `∀x. ParseTree x → Bool`... To get around this and build the liar paradox which makes the proof “go,” is not too hard: but you are basically forced to produce a quine instead and those techniques are non-trivial. In our normal programming lives, you could apply a heuristic that assumes we never do such things, and life is good. The focus on finite versus infinite memory is a huge distraction. If your halting detector applied to the above quine tried to not be a heuristic by salvaging the case where it runs out of memory while analyzing, you would get the result “this program will OOM, but if you run me in a machine with 1 meg less memory I will stop an odd number of cycles earlier and the program will not OOM, but will instead halt successfully telling you that the next cycle would OOM.” Suddenly your tests that you build with this thing are all flaky, because it didn't have the humility to be a heuristic and say “I don't know this is too complex for me,” and in the real world you are running on Linux and you don't know how many megs you really have available. Better just to not play any of that game. So yeah the problem with Turing machines is not that they have infinite memory, infinite memory is in fact a standard assumption that most programmers in GCed languages make when programming most of their programs. This is why “your problem isn't the garbage collector, it's that you're swimming in garbage” and all that. Put another way, Turing machines suck even if you enhance them to have 5 parallel tapes (God why do they not have parallel tapes by default, should have at least one for output, one for main memory, one for a stack, and some more as scratchpads) of bytes (seriously why are they still not bytes in textbooks) and enforce that the tapes each only have 1 billion symbols and any attempt to go off the edge crashes the Turing machine. You are joyous because it now only has finite memory, I can run a cycle detection with 10^{1 billion} nodes in the graph or whatever, so cycle detection is in principle solved! If you are as pragmatic as you say you are, you see that this is no help, halting is still effectively impossible.