[Solved]: Do fully optimizing compilers for terminating programs exist?

Problem Detail: 

In Andrew W. Appel's book, Modern Compiler Implementation in ML, he says under chapter 17 that Computability theory shows that it will always be possible to invent new optimizing transformations and proceeds to prove that a fully optimizing compiler will solve the halting problem: A program Q that produces no output and never halts can easily be replaced by its optimal representation, Opt(Q), being "L: goto L". So a fully optimizing compiler can solve the halting problem.

So my question is this: Does a fully optimizing compiler exist for terminating programs? My only thoughts are the following: Even though a program is guaranteed to terminate, it can still be arbitrarily complex, and for any concrete optimizing compiler, C, one could perhaps construct a program that takes C as input and somehow produces a worse program as some kind of corner case.

Also, What are the implications of restricting ourselves to terminating programs?

Asked By : Simon Shine

Answered By : Raphael

I assume you are interested in optimisation of runtime. As I've written in my comment, that does not sufficiently specify the goal: does an optimisation reduce runtime on any input, every input, all worst-case inputs or even on average?

I will show that all of them are impossible. The proof extends to optimising the length of the program.

Recall that the following problem is not computable:

Given a context-free grammar $G$ with terminal alphabet $\Sigma$, decide whether $\mathcal{L}(G) = \Sigma^*$.

Note furthermore that given a context-free grammar $G$, we can hardcode, say, the CYK algorithm for that one grammar; denote this algorithm by $\mathrm{CYK}_G$. We observe that $\mathrm{CYK}_G$ terminates for all inputs (from $\Sigma^*$).

Now assume that there is an optimiser $\operatorname{Opt}$ which, given an always terminating algorithm $A$, outputs a result-equivalent algorithm which is optimal with respect to runtime. Clearly,

$\qquad \operatorname{Opt}(\mathrm{CYK}_G) = \text{'}\mathtt{return\ true;}\text{'} \iff \mathcal{L}(G) = \Sigma^*$

and we have thus constructed a decider for an uncomputable problem, contradicting the assumption.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/13313