On 28.01.2014 10:42, "Ola Fosheim Grøstad"
<[email protected]>"@puremagic.com wrote:
On Monday, 27 January 2014 at 22:40:19 UTC, Simen Kjærås wrote:
My computer has 16GB of RAM. You try keeping track of all the possible states.
Wrong reasoning.
Correct reasoning. My reasoning is that this is infeasible, not impossible in
theory.
The issue is that the proof for the halting problem does assume non-finite
resources. That means that the proof that you cannot prove termination for an
arbitrary program does not hold for programs that run on your computer. :^)
I am well aware what the halting problem is. I'm just saying that actually
*proving* non-termination is impossible in practical situations. "This takes too
much time, let's do something else" is not a proof, but more than good enough
for most porpoises.
Anyway, the reasoning does not hold anyway, because there is an inifinite
number
of programs that can be proved to terminate… So you just do those instead!
I assume you mean finite.
From a pragmatic position speculative precomputation is quite acceptable, works
well with profiling on typical datasets and whole program analysis.
Absolutely. But just as the halting problem says that the question of whether a
program with infinite memory terminates is undecidable in general, it is
infeasible to *prove* whether a program will terminate even if memory today is
actually not infinite.
The fact that the halting problem does not apply to computers with finite memory
has no effect on deadalnix's question - it's still impossible to prove, just for
a different reason.
--
Simen
