On Tuesday, 28 January 2014 at 15:49:14 UTC, Simen Kjærås wrote:
Correct reasoning. My reasoning is that this is infeasible, not
impossible in theory.
A refutal of a proof is not required to be executed? That's not
the purpose.
"This takes too much time, let's do something else" is not a
proof, but more than good enough for most porpoises.
Then you agree with me. Good. :)
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.
No, only if you assume finite resources. Proof is trivial: you
can just add an infinite number of NOPs (like a= a+1-1) without
affecting semantics.
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.
Correction: it is infeasible to prove the termination aspects of
ALL programs. There are plenty of programs (or functions) where
you can prove it.
It depends on the program, but that doesn't matter. That was my
main point. Theoretical computer science isn't pragmatic, but
optimization is always pragmatic.
with finite memory has no effect on deadalnix's question - it's
still impossible to prove, just for a different reason.
I thought we agreed that we don't need to prove anything? You can
just bail out or do some kind of partial evaluation.
You might even want to speculatively calculate non-compile-time
functions for given parameters after profiling. Like if f(x) is
called 50% with the value x=32, then precompute and emit a
switch(x) statement with f(x) as the default and the value for
f(32) as a case.
Profiling really changes how you view these things.
