Think more like an inductive human being than a deductive formal system: “x doesn’t ever halt” would require proof, but “x really seems not to halt for a very long time and seems to contain an infinitely-growing recursion there” gives us very valid reason to believe “x doesn’t halt”, and guides us in trying to assemble a proof.
Busy beavers seem not to halt for a very long time and spend most of their time in a seemingly infinitely-growing recursion, and then they halt.
You could argue that busy beavers are pathological examples of little practical interest, but then many programs that perform useful computation may run for a very long time without entering easily identifiable “loops” before they halt. Unless you designed the program yourself and have a good understanding of what it is doing, and sometimes even if you designed the program yourself, proving termination may not be trivial.
Unless you designed the program yourself and have a good understanding of what it is doing, and sometimes even if you designed the program yourself, proving termination may not be trivial.
If it was a trivial problem it wouldn’t be worth tackling.
My point is that the observation that a program has been running for a long time and doesn’t have simple “while(true) {...}” loops doesn’t give us much information about its termination.
But I’m not sure what you are aiming at. For most practical purposes, a program that takes a very long time before producing a result is as good as a program that will never produce a result. Termination is important in theoretical computer science as the prototypical undecidable property used to prove other non-existence results, but if you are concerned about specific programs that you plan to actually run on physical machines, why are you interested in termination?
Busy beavers seem not to halt for a very long time and spend most of their time in a seemingly infinitely-growing recursion, and then they halt.
You could argue that busy beavers are pathological examples of little practical interest, but then many programs that perform useful computation may run for a very long time without entering easily identifiable “loops” before they halt.
Unless you designed the program yourself and have a good understanding of what it is doing, and sometimes even if you designed the program yourself, proving termination may not be trivial.
If it was a trivial problem it wouldn’t be worth tackling.
My point is that the observation that a program has been running for a long time and doesn’t have simple “while(true) {...}” loops doesn’t give us much information about its termination.
But I’m not sure what you are aiming at.
For most practical purposes, a program that takes a very long time before producing a result is as good as a program that will never produce a result. Termination is important in theoretical computer science as the prototypical undecidable property used to prove other non-existence results, but if you are concerned about specific programs that you plan to actually run on physical machines, why are you interested in termination?