4 ms·

> Such compiler would require solving halting problem. Wrong: Because of the finite memory instead of an unbounded tape (among other reasons), computers are st

> Such compiler would require solving halting problem. Wrong: Because of the finite memory instead of an unbounded tape (among other reasons), computers are strictly less expressive than Turing machines.

tzs 7y ago
Does the proof that the halting problem is not solvable actually make use of the unboundedness of the tape?
- wolfgke 7y ago
  Of course it does (implicitly!). Otherwise the number of possible states of the Turing machine T that we want to check whether it halts or not is finite and we just have to "simulate" the program and see whether it terminates or it reaches again a state that it was already in.
  - marcosdumay 7y ago
    How would the "if this program halts then run forever, else halt" algorithm work on a real computer? I imagine it would fail with stack overflow.
- naasking 7y ago
  Standard proof is a diagonalization, which depends on infinite sequences. That said, the Halting problem on physical computers is still of extremely high computational complexity, which can be just as high a barrier as incomputability.
h91wka 7y ago
This technically correct comment would be actually useful, if it linked a fully automated prover, that is capable of proving any property of a program that fits in N bytes. If you remove infinite tape, you go from undecidable to "just" exponentially complex.
- wolfgke 7y ago
  > If you remove infinite tape, you go from undecidable to "just" exponentially complex. Which is a huge leap - we got from "impossible" to "possible in principle" and we now can do research how to make it even "sufficiently fast" for problems of practical relevance.
  - h91wka 7y ago
    No. In CIC I can prove that, say, some property is valid for _any_ natural number. Your "memory is bounded" argument is invalid, as formal proofs can go beyond that.
h91wka 7y ago
...Also I think you don't realize that formal inductive proofs can easily reason about programs operating with unbounded memory.
- wolfgke 7y ago
  With formal inductive proofs, you can reason, but not decide.

tzs 7y ago

Does the proof that the halting problem is not solvable actually make use of the unboundedness of the tape?

wolfgke 7y ago
Of course it does (implicitly!). Otherwise the number of possible states of the Turing machine T that we want to check whether it halts or not is finite and we just have to "simulate" the program and see whether it terminates or it reaches again a state that it was already in.
- marcosdumay 7y ago
  How would the "if this program halts then run forever, else halt" algorithm work on a real computer? I imagine it would fail with stack overflow.
naasking 7y ago
Standard proof is a diagonalization, which depends on infinite sequences. That said, the Halting problem on physical computers is still of extremely high computational complexity, which can be just as high a barrier as incomputability.

h91wka 7y ago

This technically correct comment would be actually useful, if it linked a fully automated prover, that is capable of proving any property of a program that fits in N bytes. If you remove infinite tape, you go from undecidable to "just" exponentially complex.

wolfgke 7y ago
> If you remove infinite tape, you go from undecidable to "just" exponentially complex. Which is a huge leap - we got from "impossible" to "possible in principle" and we now can do research how to make it even "sufficiently fast" for problems of practical relevance.
- h91wka 7y ago
  No. In CIC I can prove that, say, some property is valid for _any_ natural number. Your "memory is bounded" argument is invalid, as formal proofs can go beyond that.

h91wka 7y ago

...Also I think you don't realize that formal inductive proofs can easily reason about programs operating with unbounded memory.

wolfgke 7y ago
With formal inductive proofs, you can reason, but not decide.