进展与保持定理

进展证明：值的类型必须决定它的形状 ​

证明先用到规范形引理：若闭值 $v$ 的类型是 Bool，则 $v$ 必为 true 或 false；若其类型为 $T_1\to T_2$，则 $v$ 必为某个 $\lambda x:T_1.t$。

引理通过检查值的语法和类型规则即可证明。它的作用是把静态判断“这是一个函数类型”，转换成动态信息“这里确实有一条 λ 应用规则可用”。只知道“子项已经是值”，还不足以完成这一步。

接着对 $\varnothing ⊢t:T$ 的类型推导做归纳。常量与 λ 抽象已经是值；空环境下不会出现自由变量分支。主要工作在应用与条件表达式。

对应用 $t_1{t}_2$，类型规则给出 $t_1:T_1\to T$ 和 $t_2:T_1$。若 $t_1$ 能走一步，应用的左侧上下文规则使整体能走一步；若 $t_1$ 已是值，再检查 $t_2$。实参能走时，使用右侧上下文规则。

最后一种情形是两者都已是值。此时规范形引理把函数值确定为 λ 抽象，于是 $\beta$ 规则适用。这排除了“函数位置已经算完，却算成了布尔值”的可能。

对 if，若条件还能归约，就在条件位置前进一步；若条件已经是值，规范形引理保证它是 true 或 false，因此总能选出一个分支。分支在被选择前无需预先执行，这与本页的求值顺序一致。

保持控制每一步后的类型；进展排除“不是值、也不能继续”的卡住状态。这张图不把类型安全等同于必定终止。

保持证明：替换实参为什么不会破坏类型 ​

保持证明的核心不是所有情况都复杂，而是 $\beta$ 步会真正改变项的结构：它把实参替换到函数体中。相应的工具是替换引理。

在绑定变量已经适当重命名、$x$ 不与环境中其他绑定冲突的约定下，若

则

这个结论准确匹配应用类型规则：函数体原本允许在 $x$ 的位置使用一个 $T_1$ 值，而实参确实提供了这种值。替换以后，原来由环境假设承担的类型依据，改由实参本身的类型推导承担。

替换必须避免变量捕获理路无捕获替换Capture-avoiding substitution用作用域感知的递归代入替换自由变量，同时保持代入项的自由变量不被捕获。。例如把自由变量 $y$ 替换进 $\lambda y.x$，不能直接得到 $\lambda y.y$，因为原来应保持自由的 $y$ 被绑定了。应先把绑定变量改名为新鲜的 $z$，再得到 $\lambda z.y$。在闭值替换的常见证明中这类冲突较少，但一般环境下的引理仍须正确处理它。

现在检查各种运行规则。对 $\beta$ 步，

经类型规则的反演，得到函数体与实参恰好满足替换引理的两个前提，故归约结果 $t[x:=v]$ 仍有类型 $T_2$。

对应用内部的归约，归纳假设说明被归约的子项保留原类型，再重新应用函数应用的类型规则即可。对条件内部的归约，同理保持条件的 Bool 类型；对选分支的规则，两个分支本来都已被要求具有同一个 $T$，因此选中任意一个都保留整体类型。

这也解释了为什么 if 类型规则必须检查两个分支，而不能只检查某次运行碰巧会执行的那一个：保持性是一项对所有合法输入和所有允许归约步骤的统一陈述。[1]

补充示意图

两个反例说明为什么需要两条定理 ​

假设保留原来的类型规则，却从动态语义中删掉 $\beta$ 归约。那么 $(\lambda x:\mathrm{Bool}.x)\mathrm{true}$ 仍是良类型闭项，却无法执行。剩余规则仍然保持类型，因此保持性本身没有发现这个问题；失败的是进展性。

反过来，假设 if 的错误类型规则只检查条件和真分支，而忽略假分支。那么

会被错误地赋予 Bool 类型。它仍能按照条件规则前进一步，但结果是函数类型的 λ 抽象，原类型没有保持。这里运行规则并不缺失，问题出在静态规则没有约束所有可能被选中的结果。

两种错误对应不同层次：进展检查良类型的形状是否有动态规则接住；保持检查动态规则的结果是否仍留在良类型集合里。把其中一个定理当作另一个的替代品，会漏掉一整类设计缺陷。

类型安全不等于终止，也不自动等于全部正确性 ​

本页的纯简单类型 λ 演算还有强规范化性质，但那是另一项定理，不能从进展与保持直接推出。若向语言加入具有合适类型规则的一般递归，仍可保持类型安全，却出现永不结束的良类型程序。

对有异常的语言，终态可能还包括规定的异常结果；对带引用的语言，状态需要包含存储，并维护存储类型；对并发语言，进展也可能要区分局部可执行性、死锁和调度假设。每一次扩展，都应明确“值”“一步”和“卡住”究竟指什么。

渐进类型理路渐进类型Gradual typing · Gradually typed lambda calculus · 渐变类型给出含函数包装的cast核心及安全性证明，并在一阶立即调用片段证明注解擦除的静态与动态渐进保证。的 cast 演算把检查失败的 blame 作为受控结果。例如未知值被要求用作整数时，布尔标签应触发 blame，而不是把布尔值交给整数原语后卡住。相应的类型安全允许这种规定的失败结果，不保证每次动态检查都成功。

同样，排除了语言定义中的类型错误，不会自动保证程序实现了用户需求、没有逻辑错误或满足某项安全策略。类型系统保证的范围，由语法、类型规则与动态语义共同决定。一个更强的类型系统可以表达更多性质，但需要相应更强的证明。

合起来怎样排除运行卡住 ​

记 ${\to }^{\ast }$ 为零步或多步归约。若初始闭项满足 $\varnothing ⊢t:T$，且

反复使用保持定理可得 $\varnothing ⊢t^{\prime }:T$。再对 $t^{\prime }$ 使用进展定理：它要么是值，要么还能走一步。于是任何可达状态都不会卡住。

例如

具有 Bool 类型，按以下顺序执行：

保持性使三项都具有 Bool 类型；进展性保证前两项确实有下一步，而最后一个布尔值是合法结束状态。类型安全的证明不是对这一个轨迹逐项检查，而是保证所有满足前提的轨迹都具有相同结构。

从论文证明到形式化与机器实现 ​

形式化这组定理时，变量绑定、上下文扩展、替换和规范形往往比主定理本身更占工作量。Software Foundations 给出了可核对的机器证明组织：先建立辅助引理，再组合进展、保持与安全性结论。[1]

若把源语言编译到SECD理路SECD 抽象机SECD machine · Stack Environment Control Dump machine通过一套明确的从左到右按值调用约定，解释 SECD 的四个部件、词法闭包、调用返回与完整执行轨迹。或其他抽象机，还需证明编译与机器执行保留源语言语义，或直接建立机器状态的类型不变量。源语言已经有进展与保持，并不自动证明任意闭包布局、栈操作或返回指令实现都正确。

这条证明路线的价值在于定位设计责任：类型规则约束程序形状，动态规则解释怎样计算，辅助引理连接绑定与替换，最终的不变量把全部运行步骤串起来。对新语言逐项完成这些连接，比仅声称“语言是类型安全的”更有内容。

函数cast核心理路渐进类型Gradual typing · Gradually typed lambda calculus · 渐变类型给出含函数包装的cast核心及安全性证明，并在一阶立即调用片段证明注解擦除的静态与动态渐进保证。在规范形中加入函数包装与ground注入，应用时反向检查参数、正向检查结果，并将blame作为受控终态。该页另对一阶立即调用片段证明注解擦除的渐进保证，明确区分单程序安全性与两程序行为比较。有限FIFO会话理路二元会话类型Binary session types · 二元会话协议从同步对偶推进到有限FIFO队列不变量，逐项证明异步保持、单会话进展与精确缓冲界。则给出另一种保持对象：局部剩余协议和两个队列必须共同推进。