保证优化：证明编译器的零空间性质(2002)

编写性能关键型程序可能会令人沮丧，因为为命令式语言优化编译器往往是不可预测的。对于优化的子集--那些简化而不是重新排序代码的优化--证明编译器可靠地执行优化将是有用的。我们表明，采用“超分析”的方法进行优化可以证明这一点。通过与线性代数类比，我们将优化器的零空间定义为它归结为空程序的程序。为了跨越空空间，我们定义了通过引入抽象来取消程序优化的重写规则。对于模型编译器，我们证明了优化器可以撤销任何反优化重写规则应用程序序列。因此，我们能够给程序员一个清晰的心理模型，说明编译器保证执行哪些简化，并在命令式语言中的“抽象惩罚”问题上取得进展。>；>；语言。>；>；