进展与保持定理 | Codeboy's Blog

形式陈述

先固定一个足够小、又能暴露证明结构的语言：带布尔值的简单类型 λ 演算。类型、项和值分别为

\begin{aligned} T&::=\mathsf{Bool}\mid T\to T,\\ t&::=x\mid\mathsf{true}\mid\mathsf{false} \mid\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t \mid\lambda x:T.t\mid t\ t,\\ v&::=\mathsf{true}\mid\mathsf{false}\mid\lambda x:T.t. \end{aligned}

采用按值调用的小步操作语义。应用先归约函数位置，再归约实参；当二者分别成为 λ 抽象和值时执行 β 步

(\lambda x:S.t_{12})\,v_2 \to t_{12}[x:=v_2].

条件式先归约守卫，并用

\mathsf{if\ true\ then}\ t_2\ \mathsf{else}\ t_3\to t_2, \qquad \mathsf{if\ false\ then}\ t_2\ \mathsf{else}\ t_3\to t_3

选择分支。类型规则包括变量、布尔常量，以及三条核心规则

\frac{\Gamma,x:S\vdash t:T}{\Gamma\vdash\lambda x:S.t:S\to T}, \qquad \frac{\Gamma\vdash t_1:S\to T\quad\Gamma\vdash t_2:S} {\Gamma\vdash t_1\,t_2:T},

\frac{\Gamma\vdash t_1:\mathsf{Bool}\quad \Gamma\vdash t_2:T\quad \Gamma\vdash t_3:T} {\Gamma\vdash\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3:T}.

对这套明确的语法、值定义和求值策略，类型安全分成两条定理：

进展（progress）：若 $\varnothing\vdash t:T$ ，则 $t\in\mathrm{Val}$ ，或者存在 $t'$ 使 $t\to t'$ ；
保持（preservation）：若 $\Gamma\vdash t:T$ 且 $t\to t'$ ，则 $\Gamma\vdash t':T$ 。

于是，如果 $t$ 是良类型闭项、 $t\to^*t'$ 且不存在 $u$ 使 $t'\to u$ ，反复使用保持可知 $\varnothing\vdash t':T$ ，再用进展便知 $t'$ 必是值。换言之，任意有限求值前缀都不会抵达一个“既不是规定结果、又没有语义后继”的卡住项。

证明部件与归纳结构

证明进展前先建立规范形式引理：若闭值 $v$ 具有布尔类型，则 $v$ 只能是 true 或 false；若闭值 $v$ 具有函数类型 $S\to T$ ，则 $v$ 只能是某个 $\lambda x:S.t$ 。它把静态类型信息转换成运行时可用的语法形状。

进展对类型推导作结构归纳。变量情形在空上下文中不可能出现；抽象与布尔常量已经是值。对应用 $t_1\,t_2$ ，归纳假设先判断 $t_1$ ：若它能走，就用应用的左侧求值规则；若它是值，规范形式引理说明它必为 λ 抽象。随后对 $t_2$ 做同样判断：实参能走便推进实参，实参是值便触发 β 步。条件式的关键完全类似，只是布尔规范形式把已成值的守卫缩成 true 或 false。

保持需要替换引理：若 $x\notin\operatorname{dom}(\Gamma)$ 、 $\Gamma,x:S\vdash t:T$ 且 $\Gamma\vdash s:S$ ，则 $\Gamma\vdash t[x:=s]:T$ 。这里的替换必须是无捕获替换。证明对 $t$ 的类型推导归纳，并在穿过 λ 绑定时处理新鲜性与上下文弱化。

随后对一步求值推导作第二次归纳。上下文规则由类型推导的逆置和归纳假设恢复；真正改变语法的 β 情形由

\Gamma,x:S\vdash t_{12}:T, \qquad \Gamma\vdash v_2:S

经替换引理推出 $\Gamma\vdash t_{12}[x:=v_2]:T$ 。条件选择从原类型规则读出两个分支具有同一类型。两条定理依赖不同归纳对象，不能用一句“按规则显然”同时略过。

直觉

进展检查的是执行路径的“前沿”：一个当前仍受类型系统认可的闭项，要么已经抵达语言承认的结果，要么至少有下一步。保持检查的是路径的“护栏”：执行一步不会把项送出原来的类型集合。沿轨迹看，保持先把类型证书交给下一个状态，进展再保证这个新状态不会意外卡死；两者交替，才能把局部证明延伸到任意有限步。

只证明进展不够，因为一项可以顺利启动，却在一次归约后变成无规则可走的坏项。只证明保持也不够：如果语义错误地不给任何项转移，那么“每次转移都保持类型”会因根本没有转移而平凡成立。类型安全来自静态规则与动态规则逐构造对齐，而不是来自“有类型”这三个字本身。

规范形式引理是这次对齐的铰链。类型推导只告诉我们函数位置具有 $S\to T$ ，小步语义却只能对 λ 抽象执行 β 规则；规范形式把前者精确翻译成后者。每加入一种新值构造、求值上下文或消去形式，都要重新检查这座桥是否完整。

例子与边界

项 true false 既不是值，也没有函数应用规则可走；类型系统会拒绝它，因为 true 不可能取得 $S\to T$ 类型。相比之下，项

(\lambda x:\mathsf{Bool}.\,\mathsf{if}\ x\ \mathsf{then\ false\ else\ true})\,\mathsf{true}

具有 Bool 类型。它先作 β 步得到 if true then false else true，再得到 false。第一步的类型保持正是替换引理的实例，第二步由条件式两个分支同型保证；每个中间项也都满足进展，直至最终值。

进展定理必须限制为闭项。开项 $x:\mathsf{Bool}\vdash x:\mathsf{Bool}$ 在给定上下文下完全良类型，但孤立变量既不是闭语言的值，也没有求值步骤；它等待环境提供含义，并不表示类型系统失败。也不能静默更改“值”与“最终状态”的定义：若语言把未捕获异常、显式 blame 或进程等待视为合法结果，就必须把它们写进定理；若不希望它们出现，则类型或效果规则还要证明更强性质。

进展与保持不推出终止。纯 STLC 的确强规范化，但那需要可归约性或逻辑关系等另一套证明；不能把这个更强结论偷塞进类型安全推论。给语言加入良类型固定点后，fix (λx:T.x) 可以永远继续，同时每一步都保持 $T$ ，所以它类型安全而不终止。类似地，两条定理不排除资源耗尽、算法超时、错误业务结果或信息泄漏，因为这些性质没有出现在当前的状态与类型判断中。

有引用时，运行对象变成项与存储的配置 $\langle t,\sigma\rangle$ ，保持要同时维护存储类型；有并发时，普通全局进展还可能被锁等待破坏，需要区分单线程可步进、全局死锁自由和调度公平。效应系统要证明实际效果受静态标注覆盖，所有权系统还要维护 owner、loan 与位置有效性。这些都是重新陈述并重证的语言定理，不是 STLC 结果的自动插件。

推论与应用

保持定理可看作“良类型配置集合对一步转移封闭”的归纳不变式，进展则排除该集合中非最终、无后继的状态。这个视角适合机械化：把类型判断、无捕获替换和小步语义编码进证明助手后，每加入一条动态规则，都必须交代它落在哪条类型规则之下；遗漏的规范形式、存储引理或绑定变量条件会变成具体未完成的证明目标。

编译器正确性还需要把这套性质跨越中间表示保存下来。源语言类型安全只说明源语义不进入指定坏状态；优化若改变求值顺序、表示或异常行为，仍需语义保持或模拟证明。字节码验证、typed assembly language 与 proof-carrying code 都复用“静态不变量对机器步封闭”的骨架，但它们的值、堆和控制栈远比 STLC 丰富。

逻辑关系、上下文等价、参数性和信息流安全回答的是更强问题：两个程序是否在所有上下文中行为一致、抽象类型是否被尊重、秘密是否影响公开观察。进展与保持是这些论证的地基，因为它们先保证观察过程本身不会落入未定义的类型错误；它们却不替代任何一项更强的行为规格。

参考资料

Andrew K. Wright and Matthias Felleisen, “A Syntactic Approach to Type Soundness,” Information and Computation 115(1), 1994, pp. 38–94。
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, §8.3。
Benjamin C. Pierce et al., Software Foundations, Volume 2: Programming Language Foundations, 2026 current edition, “Properties of STLC”.

形式陈述 ​

证明部件与归纳结构 ​

反向链接

形式陈述

证明部件与归纳结构