5 ms·

While technically correct in several ways, this is a pretty naive take on the topic. A simple counterexample is trying to decide whether a program which compute

While technically correct in several ways, this is a pretty naive take on the topic. A simple counterexample is trying to decide whether a program which computes the Collatz conjecture will always halt (which is equivalent to proving the conjecture itself). Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself. Furthermore, it is true that computers have a finite number of states, but this number is intractable for most problems in verification. There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much.

wizeman 4y ago
> Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself. 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. In fact, this would be a huge, huge deal if you could solve it in an efficient way. > There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much. I think you missed one of my points: > while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet 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 we don't know whether P=NP. And there's another issue here as well: I'm not even sure if P=NP actually has any meaning in this context, because I assume issues related to P=NP are usually analyzed in the context of Turing machines. This actually ties into the other point I mentioned: > 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?
- markusde 4y ago
  > 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
GMoromisato 4y ago
Isn't there value in a weak halt-checker? Imagine a function that always returns one of: Yes, it halts No, it loops forever Can't decide. Wouldn't that still be useful in practice?
- Nevermark 4y ago
  Yes, it could be useful. Especially if "can't decide" means "can't decide using the resources limit you provided" so that the test returns consistent results. (As apposed to different results depending on the differing resources between machines the test ran on.)
- xigoi 4y ago
  Yes, but the usefulness of such a tool depends on what exactly you want to achieve.

wizeman 4y ago

> Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself. 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. In fact, this would be a huge, huge deal if you could solve it in an efficient way. > There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much. I think you missed one of my points: > while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet 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 we don't know whether P=NP. And there's another issue here as well: I'm not even sure if P=NP actually has any meaning in this context, because I assume issues related to P=NP are usually analyzed in the context of Turing machines. This actually ties into the other point I mentioned: > 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?

markusde 4y ago
> 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

GMoromisato 4y ago

Isn't there value in a weak halt-checker? Imagine a function that always returns one of: Yes, it halts No, it loops forever Can't decide. Wouldn't that still be useful in practice?

Nevermark 4y ago
Yes, it could be useful. Especially if "can't decide" means "can't decide using the resources limit you provided" so that the test returns consistent results. (As apposed to different results depending on the differing resources between machines the test ran on.)
xigoi 4y ago
Yes, but the usefulness of such a tool depends on what exactly you want to achieve.