@dysfun @tao I think the concept of simp normal form is a bit different. It means that the subexpressions of the left hand sides of equality lemmas won't change by simp, so that you can rewrite to normal form by doing rewrites bottom up.

@krismicinski It indeed seems hard to say in general what partial evaluation is. It's probably at least a mapping from a program to a (hopefully) more efficient program. Static analysis may be even more vague, as it's a mapping from a program to "information about the program". OTOH "mapping from program to more efficient program" generally describes compiler optimization passes, so yeah. Actually, constant propagation and loop unrolling are intuitively a kind of partial evaluation. But common subexpression elimination, loop invariant code motion, loop tiling, vectorization, I'd intuitively say that those aren't partial evaluation...and dead code limination? Who knows.