I don't think this will allow solving the halting problem, its been mathematically proved to be impossible to solve [1].
Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
> I don't think this will allow solving the halting problem, its been mathematically proved to be impossible to solve [1].
Yes, this is my point: the proposed super-optimiser would, it seems to me, en passant be solving the halting problem, which means that it can't actually exist (or, at least, can't actually satisfy the stated guarantee).
> Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
On the level of the lambda-calculus, this is reflected in the corresponding term's having no normal form, in which case the algorithm described (which relies on reducing everything to a normal form) cannot do anything with it.
The halting problem forbids the existence of oracles which can decide with certainty in some finite time that an arbitrary program will halt. Loosen any of these qualifiers and the problem is not necessarily undecidable. Loosening the "arbitrary program" restriction, the problem of analyzing the termination of a subset of programs which doesn't encode looping or recursion constructs ( i.e. simply typed lambda calculus ) is trivially decidable. A totality checker like in Agda can decide whether some programs halt given a set of restrictions on the program.
Nothing prevents a turing complete program from entering an infinite loop. A GUI program for example is terminated only when the user decides to, which is impossible to predict.
1. http://en.wikipedia.org/wiki/Rice%27s_theorem