Comment by twoodfin
3 years ago
I’m curious: Has there been any research on optimization in the opposite direction? Start with the most naively implemented correct function—a giant switch/nested if covering all possible inputs—and transform it piecewise in a correctness-preserving manner?
A similar problem comes up in digital design. Behaviour is often specified in terms of exhaustive truth tables, perhaps tables that were generated automatically, from a hardware description language. While such a table can be directly translated into a circuit, doing so in a naive fashion is potentially extremely non-optimal. Optimizing it is a hard problem. Everything has been tried, from exhaustive search (suitable only for small numbers of terms), to rule-based fuzzy backtracking searches, to in recent years, deep learning. But at least when I was in school a couple decades ago, the best known algorithm was still a person playing with the terms on graph paper, rearranging them until patterns emerged: https://en.wikipedia.org/wiki/Karnaugh_map
As I understand it, there are recent advances in SAT solvers giving practical algorithms for much larger numbers of terms, but I'm much behind the state of the art at this point.
I've done this. In my experience it ends up stuck in local minima from which there are no obvious correctness-preserving improvements. Add Monte Carlo to escape valleys and this mode of exploration is still too timid to find anything close to optimal.
When you find a truly optimal solution, you end up with the least satisfying proof of correctness: "Here's this this inscrutable formula; I verified that it produces the right output for all possible inputs."
Mostly yes. There is a lot of research on taking arbitrary programs and distilling constraints and invariants out of them or doing various forms of function simplification.