5 ms·

> What I am saying is that in practice, for the huge majority of interesting problems, it is not useful to finitize the actual program but instead to abstract o

> What I am saying is that in practice, for the huge majority of interesting problems, it is not useful to finitize the actual program but instead to abstract over the program that assumes no meaningful resource constraints. Wandering off down a road of looking for efficient algorithms that take advantage of the actual finite nature of real programs will only harm you in the enormous majority of cases. You may very well be correct, but there's no formal result that proves that, right? So your assertion could be wrong. > Again, people only "get it wrong" if you are being maximally pedantic in a way that provides negative value to thinking about these problems. If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms. Fortunately, some people have proven that these algorithms exist and have created such algorithms. Some have even created new such algorithms, improving their efficiency. I just want more people to try and find more efficient versions of those, which is why we should not be spreading mistaken beliefs that the Halting problem is undecidable when a program runs on a computer. Which is why I would argue, in fact, that saying the Halting problem is undecidable is what provides negative value, because this is only of theoretical interest and generally speaking, it's only a useful result in practice if the program you're analyzing is trying to solve a mathematical question (i.e. one about infinity). For most real-world programs, the question of whether they would halt (or whether they behave correctly, in general) if they weren't allowed to consume infinite memory is much more interesting and useful, and actually decidable! So let's focus instead on improving the time complexity of such algorithms. Let's not focus on saying that they are impossible to solve, which prevents from focusing on the former.

School-Cotton 4y ago
> You may very well be correct, but there's no formal result that proves that, right? GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world. > If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms. This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible.
- wizeman 4y ago
  > GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world. Ok, I see your points. > This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible. It doesn't? I thought the halting problem was the problem of constructing an algorithm that decides whether a machine that runs an arbitrary program will keep cycling between states or not (which in the case of a Turing machine, includes the state of the tape). If you say it's undecidable, it implies no such algorithm can exist.
  - School-Cotton 4y ago
    > If you say it's undecidable, it implies no such algorithm can exist. It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines. It does not imply that “cycle detection” is an impossible task under any circumstances, possibly on different classes of graphs, or possibly sacrificing strict correctness. I honestly think you understand this and are just being intentionally obtuse.
    - wizeman 4y ago
      > It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines. Yes, what you said is strictly correct, but that's not how the Halting problem is usually presented nor how it is usually understood. Normally, you don't hear people saying: "the Halting problem is undecidable for Turing machines", and that's it, everybody understands what's going on and the limitations of that statement. Instead, it is usually said: "The Halting problem is undecidable". And then they say: "Here, let me show you that it's undecidable using this clever proof, which uses a Turing machine as a model". And then, more crucially, they don't say "But of course, this proof is completely wrong if you assume that the program runs on a finite-state machine. And not just that, but it is proven that it is decidable in such circumstances". > I honestly think you understand this and are just being intentionally obtuse. I understand in general, but I might misunderstand particular statements in some precise way. I'm not intentionally being obtuse, I promise you. There's a lot of nuance in this topic and when we're not being mathematically precise it's easy to misunderstand each other.
UncleMeat 4y ago
> You may very well be correct, but there's no formal result that proves that, right? So your assertion could be wrong. The entire thread started off by you rejecting the formalism provided by folks like Turing in favor of the practical argument. I'm speaking from a practical perspective of building actual static analysis tools. When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best. > If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms. No that's not true. Not at all. We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice. We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems. There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time. Actual deployed algorithms have some number of false positives or false negatives (or both).
- wizeman 4y ago
  > When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best. That's not what I'm arguing at all. I'm arguing that as long as you restrict the programs being analyzed to the subset of programs that use a finite amount of memory (i.e. those that can run on a computer), then all so-called undecidable theories suddenly become decidable. And that this could be a property that we could perhaps exploit to analyze programs more efficiently. But you don't have to make your models more complicated. It's simply a property that you can exploit, whenever you want to. > We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice. Exactly. Wouldn't it be better if you could always have true positives and true negatives? To be clear, I'm not saying that we can do this right now. But it's an avenue worth pursuing, IMHO. > We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems. It is decidable, that's my entire point! If there's a finite amount of memory, the theories become decidable! Perhaps you're just confusing time complexity with decidability? > There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time. Exactly, there isn't! Which is why we should find one that terminates in a reasonable amount of time. That's what I'm arguing. > Actual deployed algorithms have some number of false positives or false negatives (or both). Agreed.

School-Cotton 4y ago

> You may very well be correct, but there's no formal result that proves that, right? GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world. > If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms. This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible.

wizeman 4y ago
> GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world. Ok, I see your points. > This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible. It doesn't? I thought the halting problem was the problem of constructing an algorithm that decides whether a machine that runs an arbitrary program will keep cycling between states or not (which in the case of a Turing machine, includes the state of the tape). If you say it's undecidable, it implies no such algorithm can exist.
- School-Cotton 4y ago
  > If you say it's undecidable, it implies no such algorithm can exist. It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines. It does not imply that “cycle detection” is an impossible task under any circumstances, possibly on different classes of graphs, or possibly sacrificing strict correctness. I honestly think you understand this and are just being intentionally obtuse.
  - wizeman 4y ago
    > It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines. Yes, what you said is strictly correct, but that's not how the Halting problem is usually presented nor how it is usually understood. Normally, you don't hear people saying: "the Halting problem is undecidable for Turing machines", and that's it, everybody understands what's going on and the limitations of that statement. Instead, it is usually said: "The Halting problem is undecidable". And then they say: "Here, let me show you that it's undecidable using this clever proof, which uses a Turing machine as a model". And then, more crucially, they don't say "But of course, this proof is completely wrong if you assume that the program runs on a finite-state machine. And not just that, but it is proven that it is decidable in such circumstances". > I honestly think you understand this and are just being intentionally obtuse. I understand in general, but I might misunderstand particular statements in some precise way. I'm not intentionally being obtuse, I promise you. There's a lot of nuance in this topic and when we're not being mathematically precise it's easy to misunderstand each other.

UncleMeat 4y ago

> You may very well be correct, but there's no formal result that proves that, right? So your assertion could be wrong. The entire thread started off by you rejecting the formalism provided by folks like Turing in favor of the practical argument. I'm speaking from a practical perspective of building actual static analysis tools. When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best. > If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms. No that's not true. Not at all. We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice. We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems. There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time. Actual deployed algorithms have some number of false positives or false negatives (or both).

wizeman 4y ago
> When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best. That's not what I'm arguing at all. I'm arguing that as long as you restrict the programs being analyzed to the subset of programs that use a finite amount of memory (i.e. those that can run on a computer), then all so-called undecidable theories suddenly become decidable. And that this could be a property that we could perhaps exploit to analyze programs more efficiently. But you don't have to make your models more complicated. It's simply a property that you can exploit, whenever you want to. > We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice. Exactly. Wouldn't it be better if you could always have true positives and true negatives? To be clear, I'm not saying that we can do this right now. But it's an avenue worth pursuing, IMHO. > We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems. It is decidable, that's my entire point! If there's a finite amount of memory, the theories become decidable! Perhaps you're just confusing time complexity with decidability? > There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time. Exactly, there isn't! Which is why we should find one that terminates in a reasonable amount of time. That's what I'm arguing. > Actual deployed algorithms have some number of false positives or false negatives (or both). Agreed.