5 ms·

> I don't agree at all. I do static analysis for my career. Trying to model the actual set of available memory configurations of a physical machine is going to

> I don't agree at all. I do static analysis for my career. Trying to model the actual set of available memory configurations of a physical machine is going to scale way way way worse for most meaningful problems than approaching this the usual way. I don't really understand your argument. I didn't say anything about how you need to solve problems like those described by the Halting problem and Rice's theorem for finite-state machines. So I'm not constraining how you would have to solve this issue. You can model the memory configuration if you want. But you don't have to model it in your algorithm. It's just that your algorithm is allowed to assume that the amount of memory available for the program being analyzed is finite (if it wants to). But anyway, the complexity / efficiency of an algorithm that solves the problem is a different issue that than the decidability of the problem, the latter of which many people get it wrong.

UncleMeat 4y ago
> So I'm not constraining how you would have to solve this issue. You can model the memory configuration if you want. But you don't have to model it in your algorithm. It's just that your algorithm is allowed to assume that the amount of memory available for the program being analyzed is finite (if it wants to). 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. > But anyway, the complexity / efficiency of an algorithm that solves the problem is a different issue that than the decidability of the problem, the latter of which many people get it 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.
- wizeman 4y ago
  > 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

> So I'm not constraining how you would have to solve this issue. You can model the memory configuration if you want. But you don't have to model it in your algorithm. It's just that your algorithm is allowed to assume that the amount of memory available for the program being analyzed is finite (if it wants to). 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. > But anyway, the complexity / efficiency of an algorithm that solves the problem is a different issue that than the decidability of the problem, the latter of which many people get it 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.

wizeman 4y ago
> 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.