4 ms·

Has it been proven that the ability to write undecidable programs confers expressive power such that you can't have one without the other? It seems self-evident

Has it been proven that the ability to write undecidable programs confers expressive power such that you can't have one without the other? It seems self-evident that running forever can't be useful, so you should be able to say WLOG that useful programs always halt. So the set of all useful programs is strictly smaller than the set of Turing machines. Is there a formal reason why Turing machines are desirable?

lisper 13y ago
> Has it been proven that the ability to write undecidable programs confers expressive power such that you can't have one without the other? Yes. > It seems self-evident that running forever can't be useful Really? Do you not think that it might be useful for, say, an operating system to run forever?
- mtdewcmu 13y ago
  >> Has it been proven that the ability to write undecidable programs confers expressive power such that you can't have one without the other? Yes. Can you provide a reference? >> It seems self-evident that running forever can't be useful Really? Do you not think that it might be useful for, say, an operating system to run forever? It's nice when the OS has the option of shutting down deterministically.
- caf 13y ago
  Do you think it is useful to implement an operating system entirely at compile-time, in an implementation which uses separate compile and run phases?
  - mtdewcmu 13y ago
    I'm not sure I follow what you're talking about. Operating Systems are tangential to the point, though. When I said all useful programs halt, the kinds of programs I meant are the kind used to prove things about computation. Those programs are simplified abstractions of real programs, and they generally compute one result and then halt (if they halt). Being simple makes those programs easier to use in proofs than real programs. However, the proofs still generalize to real programs; a real-world program with multiple functions is equivalent to several single-function programs glued together together. So my point in saying that all useful programs halt was really to argue that all useful programs must have the constraint that they their behavior is always predictable, or controllable, in some sense. In a trivial way, computers are always predictable, but Turing proved that there are cases where it's impossible to predict the eventual outcome of a program in advance, i.e., the halting problem. In precise terms, the outcome (halt/not halt) of some programs is said to be undecidable or uncomputable. Undecidability is a hallmark of Turing machines. But since real programs are written by humans, who can't solve undecidable problems, real programs will never be able to gain any advantage from undecidable behavior.

lisper 13y ago

> Has it been proven that the ability to write undecidable programs confers expressive power such that you can't have one without the other? Yes. > It seems self-evident that running forever can't be useful Really? Do you not think that it might be useful for, say, an operating system to run forever?

mtdewcmu 13y ago
>> Has it been proven that the ability to write undecidable programs confers expressive power such that you can't have one without the other? Yes. Can you provide a reference? >> It seems self-evident that running forever can't be useful Really? Do you not think that it might be useful for, say, an operating system to run forever? It's nice when the OS has the option of shutting down deterministically.
caf 13y ago
Do you think it is useful to implement an operating system entirely at compile-time, in an implementation which uses separate compile and run phases?
- mtdewcmu 13y ago
  I'm not sure I follow what you're talking about. Operating Systems are tangential to the point, though. When I said all useful programs halt, the kinds of programs I meant are the kind used to prove things about computation. Those programs are simplified abstractions of real programs, and they generally compute one result and then halt (if they halt). Being simple makes those programs easier to use in proofs than real programs. However, the proofs still generalize to real programs; a real-world program with multiple functions is equivalent to several single-function programs glued together together. So my point in saying that all useful programs halt was really to argue that all useful programs must have the constraint that they their behavior is always predictable, or controllable, in some sense. In a trivial way, computers are always predictable, but Turing proved that there are cases where it's impossible to predict the eventual outcome of a program in advance, i.e., the halting problem. In precise terms, the outcome (halt/not halt) of some programs is said to be undecidable or uncomputable. Undecidability is a hallmark of Turing machines. But since real programs are written by humans, who can't solve undecidable problems, real programs will never be able to gain any advantage from undecidable behavior.