4 ms·

> - 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 y

> - 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.
- Khoth 4y ago
  > 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) You answered your question as you asked it. If you juice up your Turing machine like that, it will still suck so much that nobody will actually write programs for it, but it will be more complicated to describe and analyse.
  - kaba0 4y ago
    I think he/she was just “sarcasticly” extending Turing machines to show that even in practicality its limits apply. But for those who may not know, you can emulate an n-tape Turing machine with a single-tape one, they are computationally equivalent (and in fact, there is no stronger model of computability)
  - wizeman 4y ago
    > You answered your question as you asked it. If you juice up your Turing machine like that, it will still suck so much that nobody will actually write programs for it, but it will be more complicated to describe and analyse. Of course. Why would you do that? You don't have to. You can write a program in a Turing-complete language and yet analyze how it will run on a machine with a finite amount of memory. For example, when you analyze cycle detection algorithms, which assume that the program being analyzed runs on a machine with a finite amount of states (even if it is implemented in a Turing-complete language), you don't do any of that. And the currently-known algorithms are very simple to analyze.
- wizeman 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 what does that say about the problem, that current SMT solvers fail? It only implies that it's a difficult problem to solve (i.e. that the time complexity may be large, possibly), but it doesn't prove that it necessarily has to be that way. > (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.) I don't think the Halting problem proves anything about the complexity of the problem or whether you can only apply heuristics and not solve the problem in a principled way. In fact, cycle detection algorithms work deterministically, without any use of heuristics. The proof of the Halting problem only works because in Turing machines, programs are allowed to consume memory infinitely without ever running into a cycle. If you don't allow that, then the Halting theorem doesn't say anything. > This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language You mean, Turing-complete languages. In which case I agree, normal programming languages also make the simplifying assumption that the computer has infinite memory. Which is actually OK! That these programs are written in such languages doesn't prevent an algorithm from determining whether an arbitrary program written in such a language will halt or not, if it were to be executed in a machine with a finite amount of memory. > 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.” Yes, exactly! > 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. Actually, I would argue that it would be immensely useful to be able to run such a tool and that it would tell me: "Hey, your program will OOM even if you run it with 1 TB of memory!" Or even, say, 16 GB of memory. Of course, with this value being configurable. And also, take into consideration that you'd be able to know exactly why that happens. > 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. Yes, and I see nothing wrong with that. Although I would like a tool like described above which would determine whether my program is buggy. > 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 Sure, but why would you do that? When analyzing cycle detection algorithms (which assume a finite amount of possible states) you don't do any of that crap :) > 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. Yes, it's solved! Awesome! Not let's focus on how to reduce the time complexity, which is the actual important problem! And don't assume that cycle detection needs to run a program step by step through all of the states of the program.
School-Cotton 4y ago
> Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me. By your definition, all problems of the form “does program X have property Y” are decidable, because you can just simulate X on all possible inputs until it halts or cycles, and observe whether Y holds in each case.
- wizeman 4y ago
  > By your definition, all problems of the form “does program X have property Y” are decidable, because you can just simulate X on all possible inputs until it halts or cycles, and observe whether Y holds in each case. Yes! Thank you! That's exactly what I'm saying. Now the question is: how can we do this without having to simulate running the program step-by-step on all possible inputs? Or in other words, how can we reduce the time complexity of the currently-known algorithms for solving this problem? That's the actual interesting question!
  - Nevermark 4y ago
    Ok, but unless you stick with some fixed resource limit N forever, the problem is undecidable again. I suppose we could pick a very large resource number N (allocatable between time and memory space?) and agree that we will create a large body of math and algorithms with the assumption of that limit, so all our theorems and programs within that finite math area are consistent. But a great deal of math would have to be reconsidered every time N was increased.
    - wizeman 4y ago
      > Ok, but unless you stick with some fixed resource limit N forever, the problem is undecidable again. Why do you believe that? The existence of the cycle detection algorithms that I mentioned earlier don't assume any particular number N and yet they prove that the problem is decidable as long as N is assumed to be a finite number.
      - Nevermark 4y ago

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.

Khoth 4y ago
> 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) You answered your question as you asked it. If you juice up your Turing machine like that, it will still suck so much that nobody will actually write programs for it, but it will be more complicated to describe and analyse.
- kaba0 4y ago
  I think he/she was just “sarcasticly” extending Turing machines to show that even in practicality its limits apply. But for those who may not know, you can emulate an n-tape Turing machine with a single-tape one, they are computationally equivalent (and in fact, there is no stronger model of computability)
- wizeman 4y ago
  > You answered your question as you asked it. If you juice up your Turing machine like that, it will still suck so much that nobody will actually write programs for it, but it will be more complicated to describe and analyse. Of course. Why would you do that? You don't have to. You can write a program in a Turing-complete language and yet analyze how it will run on a machine with a finite amount of memory. For example, when you analyze cycle detection algorithms, which assume that the program being analyzed runs on a machine with a finite amount of states (even if it is implemented in a Turing-complete language), you don't do any of that. And the currently-known algorithms are very simple to analyze.
wizeman 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 what does that say about the problem, that current SMT solvers fail? It only implies that it's a difficult problem to solve (i.e. that the time complexity may be large, possibly), but it doesn't prove that it necessarily has to be that way. > (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.) I don't think the Halting problem proves anything about the complexity of the problem or whether you can only apply heuristics and not solve the problem in a principled way. In fact, cycle detection algorithms work deterministically, without any use of heuristics. The proof of the Halting problem only works because in Turing machines, programs are allowed to consume memory infinitely without ever running into a cycle. If you don't allow that, then the Halting theorem doesn't say anything. > This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language You mean, Turing-complete languages. In which case I agree, normal programming languages also make the simplifying assumption that the computer has infinite memory. Which is actually OK! That these programs are written in such languages doesn't prevent an algorithm from determining whether an arbitrary program written in such a language will halt or not, if it were to be executed in a machine with a finite amount of memory. > 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.” Yes, exactly! > 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. Actually, I would argue that it would be immensely useful to be able to run such a tool and that it would tell me: "Hey, your program will OOM even if you run it with 1 TB of memory!" Or even, say, 16 GB of memory. Of course, with this value being configurable. And also, take into consideration that you'd be able to know exactly why that happens. > 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. Yes, and I see nothing wrong with that. Although I would like a tool like described above which would determine whether my program is buggy. > 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 Sure, but why would you do that? When analyzing cycle detection algorithms (which assume a finite amount of possible states) you don't do any of that crap :) > 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. Yes, it's solved! Awesome! Not let's focus on how to reduce the time complexity, which is the actual important problem! And don't assume that cycle detection needs to run a program step by step through all of the states of the program.

School-Cotton 4y ago

> Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me. By your definition, all problems of the form “does program X have property Y” are decidable, because you can just simulate X on all possible inputs until it halts or cycles, and observe whether Y holds in each case.

wizeman 4y ago
> By your definition, all problems of the form “does program X have property Y” are decidable, because you can just simulate X on all possible inputs until it halts or cycles, and observe whether Y holds in each case. Yes! Thank you! That's exactly what I'm saying. Now the question is: how can we do this without having to simulate running the program step-by-step on all possible inputs? Or in other words, how can we reduce the time complexity of the currently-known algorithms for solving this problem? That's the actual interesting question!
- Nevermark 4y ago
  Ok, but unless you stick with some fixed resource limit N forever, the problem is undecidable again. I suppose we could pick a very large resource number N (allocatable between time and memory space?) and agree that we will create a large body of math and algorithms with the assumption of that limit, so all our theorems and programs within that finite math area are consistent. But a great deal of math would have to be reconsidered every time N was increased.
  - wizeman 4y ago
    > Ok, but unless you stick with some fixed resource limit N forever, the problem is undecidable again. Why do you believe that? The existence of the cycle detection algorithms that I mentioned earlier don't assume any particular number N and yet they prove that the problem is decidable as long as N is assumed to be a finite number.
    - Nevermark 4y ago