形式陈述

进展：若 $\varnothing\vdash t:T$$\varnothing ⊢t:T$，则 $t$$t$ 是值，或存在 $t'$$t^{\prime }$ 使 $t\to t'$$t\to t^{\prime }$。保持：若 $\Gamma\vdash t:T$$\mathrm{\Gamma }⊢t:T$ 且 $t\to t'$$t\to t^{\prime }$，则 $\Gamma\vdash t':T$$\mathrm{\Gamma }⊢t^{\prime }:T$。二者共同给出“well-typed programs do not go wrong”的精确定义。

直觉

进展排除无规则可走的中间状态；保持保证每走一步，静态类型给出的承诺仍然成立。

例子与边界

STLC 中，把函数应用到匹配类型的实参可以继续归约。定理不保证程序终止，也不保证没有除零、资源耗尽等未编码进类型的错误。

推论与应用

进展与保持是证明语言类型安全的标准分解，也指导新类型规则和运行时语义的设计。

参考资料

• Andrew K. Wright and Matthias Felleisen, “A Syntactic Approach to Type Soundness,” 1994.
• Benjamin C. Pierce, Types and Programming Languages, §8.3.