Daniel Berlin wrote:
The chain of inferences that the compiler would need to do to properly
diagnose this case is beyond the scope of the mechanical transformations.
The reasoning you need to implement to catch these cases could even be
reduced to the halting problem.
I hate to bring this up, because it's a "half-troll", but the halting
problem is *not* undecidable on the machines we use everyday, because they
have finite memory.
This is theoretically true, but quite irrelevant, any "solution" to such
problems is likely exponentional and totally out of the question.
The halting problem *is* solvable for finite machines (and indeed, if it
wasn't, we'd be in serious trouble).
http://doi.acm.org/10.1145/1052796.1052798
It's one thing to say it's beyond of the scope of the mechanical
transformations we want to do, but reduction to the halting problem is
usually just a punt :)
On the contrary, it is the introduction of this theoretical red herring
that is the punt.
Furthermore it is not operationally true, since you can write files that
are from a
practical point of view unlimited in length.
It would be interesting if you could give an example where an undecidable
property of a program is actually decided on the basis of finiteness in
a real
world context. I know of no such examples.
