10
$\begingroup$

Circuit Minimization is the problem to minimize the size of a given circuit. Is there anything similar for general programs?

In particular my question is -

Do there exist algorithms to minimize the # of instructions for a given program. I know it's an undecidable problem but I'm not looking for a solution that returns something optimal.

While one can apply preexisting compiler transformations to accomplish this, I'm looking for something where I don't have to define a set of very narrow transformations and algorithms to search for them beforehand.

Edit: The other question I have is whether one can have a calculus that is sound and complete that allows us to explore the whole space of such semantically equivalent programs or is that not possible.

$\endgroup$
  • 2
    $\begingroup$ The answer to your other question depends on your definition of "a calculus". $\:$ The fact that HALT is not in coRE makes the answer "no" for most such definitions. $\;\;\;\;$ $\endgroup$ – user6973 Mar 10 '14 at 22:23
  • $\begingroup$ the two fields are related in that another approach is to convert the programs to the family of circuits for varying input sizes $f_n$ $\endgroup$ – vzn Mar 11 '14 at 20:16
10
$\begingroup$

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove that the program is equivalent to the original, stop; otherwise keep searching.

This algorithm is sound. In order for it to be complete, you need to be able to prove all rejected programs are not equivalent to the original. This is possible in finitary machine models, as long as you have a bound for the input size.

Note that when the program execution time depends on the input, there may not be an optimal solution. If you look for e.g. a worst-case bound, you'll very quickly run into undecidable equivalences when you quantify over all possible unbounded inputs, and into untractable problems if the inputs are bounded.

A decade ago, “Denali: A Goal-Directed Superoptimizer” by Rajeev Joshi , Greg Nelson and Keith Randall was able to find optimal programs of about 5 machine instructions. I haven't looked at more recent results.

$\endgroup$
  • 5
    $\begingroup$ One of our students here at the University of Sussex used superoptimisation to shorten the length of some core Java routine (such as addition). He burned enormous amounts of Amazon EC2 computation to do this. His dissertation is here. Clearly not a feasible approach for anything but really short programs. $\endgroup$ – Martin Berger Mar 11 '14 at 12:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.