3 ms·

I don't think a theoretical computer scientist would agree.

bluGill 3y ago
So long as the number of states is finite theory says we can prove by exhaustion. Either a state terminates, or it becomes a different state. Then you do a tree seach until you have reached a termination or a state already in the tree. You need more memory than the number of states to do this, but theroy allows for infine memory in the proof.
- bluGill 3y ago
  Remember the halting problem is proving within a system, we can often step outside the system to prove it. Which sometimes allowes for more properties to be proved'
  - drdeca 3y ago
    The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is no system in which things need proving. Instead, the analogous thing is that, for any program that returns one of “halts”, “doesn’t halt”, or “unknown” and only returns the first two in cases where those are correct, there are other machines which also do that, but where they answer “unknown” for a smaller set of inputs. (E.g. you can just augment the program by hard-coding in the correct value for some input that it previously answered “unknown” for.) Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.
- deterministic 3y ago
  Computer scientists routinely prove theories with an infinite number of states. It is actually usually the easiest way to prove things because you don’t have to handle edge cases. A typical theory says: For all x:A, P x In other words, given any x (from an infinite set A) P x is true. Where P is a proposition. You typically prove it using straightforward induction/recursion.

So long as the number of states is finite theory says we can prove by exhaustion. Either a state terminates, or it becomes a different state. Then you do a tree seach until you have reached a termination or a state already in the tree. You need more memory than the number of states to do this, but theroy allows for infine memory in the proof.

bluGill 3y ago
Remember the halting problem is proving within a system, we can often step outside the system to prove it. Which sometimes allowes for more properties to be proved'
- drdeca 3y ago
  The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is no system in which things need proving. Instead, the analogous thing is that, for any program that returns one of “halts”, “doesn’t halt”, or “unknown” and only returns the first two in cases where those are correct, there are other machines which also do that, but where they answer “unknown” for a smaller set of inputs. (E.g. you can just augment the program by hard-coding in the correct value for some input that it previously answered “unknown” for.) Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.
deterministic 3y ago
Computer scientists routinely prove theories with an infinite number of states. It is actually usually the easiest way to prove things because you don’t have to handle edge cases. A typical theory says: For all x:A, P x In other words, given any x (from an infinite set A) P x is true. Where P is a proposition. You typically prove it using straightforward induction/recursion.