Combining Optimizations, Combining Theories

We consider the problem of how best to combine optimizations in imperative compilers. It is known that combined optimizations (or "super-analyses") can be strictly better than iterating separate improvement passes. We propose an explanation of why this is so by drawing connections between program analysis and the algebraic and coalgebraic views of programs and processes. We argue that "optimistic" analyses decide coinductively-defined relations and are based on bisimilarity