. 类型安全：典范形式、进展与保型

Glomzzz
2026-10-10
About

通过典范形式引理、进展定理与保型定理，证明算术语言的良类型词项求值不会受阻．

1 先把命题写下来

“良类型的程序不会出错”这句话， Robin Milner 在 1978 年说成 well-typed programs cannot go wrong．要把它写成精确命题，必须先规定“出错”是什么：本文只指规约到受阻状态，即非值且没有后继的词项（正规形式与受阻），不涉及异常、资源耗尽或业务逻辑错误．

要证明的类型安全性表达了类型规则与执行规则之间的协调．文献常把这类保证称为类型健全性；本文在这一“不受阻”的意义下使用它（注意与检查器相对类型规则的“算法可靠性”区分）．

Definition 1.1 类型安全 [type-safety]

2026-10-10
Glomzzz

采用类型与类型判断的类型关系、多步规约的运行关系，以及正规形式与受阻的受阻判定．称这套语言规则具有类型安全性，如果对任意词项 $𝑡$ 、 $𝑡^{'}$ 和类型 $𝑇$ ：若 $𝑡 : 𝑇$ 且 $𝑡 ⟶^{*} 𝑡^{'}$ ，则 $𝑡^{'}$ 没有受阻．

这个性质表达了类型规则相对于执行规则的类型健全性：良类型词项的执行不会进入所定义的错误状态．它不直接涉及某个具体检查算法，也不承诺终止或排除真实语言中的所有运行时错误．

注意这句话里的量词：对所有良类型的 $𝑡$ ，对所有它能多步规约到的 $𝑡^{'}$ ．这正是量词的范围提醒过的地方；写成符号以后，范围就不会有歧义．

直接证明这个命题不好下手，因为 $⟶^{*}$ 可以规约任意多步． Andrew K. Wright 与 Matthias Felleisen 在 1994 年给出的办法，是把它拆成两条只涉及一步的定理：进展说良类型的项要么是值、要么还能一步规约，保证“当前不受阻”；保型说良类型的项一步规约后得到的项类型不变，保证“规约一步以后，进展还能接着用”．

两条缺一不可．规约到受阻里的 $succ (if true then false else 0)$ 现在能规约，一步规约之后就受阻了．只有进展，挡不住这种情况；只有保型，挡不住一开始就受阻的项（这个例子本身没有类型，只是借来说明两条定理各自守住的防线）．

2 典范形式

证明进展时需要知道：某个类型的值长什么样．

Lemma 2.1 典范形式 [canonical-forms]

2026-10-10
Glomzzz

值与数值使用值与数值的定义，类型关系使用类型与类型判断．第 1 条，若 $𝑣$ 是值且 $𝑣 : Bool$ ，则 $𝑣$ 是 $true$ 或 $false$ ；第 2 条，若 $𝑣$ 是值且 $𝑣 : Nat$ ，则 $𝑣$ 是数值．

Proof.

由值与数值，值只有三种形状：

true

、

false

、数值．对第 1 条，若

𝑣

是数值，它是

0

（由反演第 1 条，类型只能是

Nat

）或

succ nv

（由第 3 条，类型只能是

Nat

）；由类型唯一，它不可能同时具有类型

Bool

，所以类型为

Bool

的值只能是

true

或

false

．对第 2 条，由反演第 1 条，

true

、

false

的类型只能是

Bool

，所以类型为

Nat

的值只能是数值．

∎

这条引理把静态信息和动态信息连了起来．它的前提 $𝑣 : Bool$ 是类型信息，类型检查器不运行程序就能在编译期得出；它的结论“ $𝑣$ 是 $true$ 或 $false$ ”是形状信息，说的是这个值具体长什么样，而求值规则只认形状．进展的证明正是靠它，从“条件是 $Bool$ 类型的值”推出“条件确实是 $true$ 或 $false$ ”，才能选择 E-IfTrue 或 E-IfFalse．反过来，若随意加一条定型规则 $0 : Bool$ ，却不改求值规则， $if 0 then true else false$ 就能通过类型检查；但没有任何求值规则能处理它，所以会受阻：它的类型是布尔值，形状却与已有求值规则要求的 $true$ 或 $false$ 不符．动态语言在运行时做的种类检查，正是在实际运行到该位置时才检查这类形状条件．

Note 2.2 静态类型与动态类型 [static-and-dynamic-typing]

2026-10-10
Glomzzz

打开独立页面 →

3 进展

进展回答的是“类型检查通过以后，下一步会不会无规则可用”．没有它，检查器即使给出了类型，也未必挡住 $succ true$ 这样的错误．具体地，若把 T-Succ 的前提错误放宽成 $𝑡_{1} : Bool$ ，这个项就会得到类型 $Nat$ ，却既非值又不能规约．进展还必须允许“已经是值”这个分支，否则 $0$ 这种合法结果反而会判为失败．对于有异常的真实语言，则要先明确哪些异常是许可的结果，不能把本文的进展原封不动当作“永不抛异常”．

Theorem 3.1 进展 [progress]

2026-10-10
Glomzzz

采用类型与类型判断的类型关系、值与数值的值定义，以及一步规约的规约关系．若 $𝑡 : 𝑇$ ，则 $𝑡$ 是值，或存在 $𝑡^{'}$ 使 $𝑡 ⟶ 𝑡^{'}$ ．

Proof.

对 $𝑡 : 𝑇$ 作规则归纳（类型推导版本的规则归纳法），按最后一步的规则分情形．

若最后一步是 T-True、T-False 或 T-Zero，则 $𝑡$ 本身就是值．若最后一步是 T-If，则 $𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ，前提里有 $𝑡_{1} : Bool$ ；对 $𝑡_{1}$ 用归纳假设，若 $𝑡_{1}$ 能规约，由 E-If 知 $𝑡$ 也能规约；若 $𝑡_{1}$ 是值，由典范形式第 1 条知它是 $true$ 或 $false$ ，可分别用 E-IfTrue、E-IfFalse．若最后一步是 T-Succ，前提为 $𝑡_{1} : Nat$ ；若 $𝑡_{1}$ 能规约，用 E-Succ；若 $𝑡_{1}$ 是值，由典范形式第 2 条知它是数值 $nv$ ，于是 $t = succ nv$ 本身也是数值，自然也是值．若最后一步是 T-Pred，前提为 $𝑡_{1} : Nat$ ；若 $𝑡_{1}$ 能规约，用 E-Pred；若 $𝑡_{1}$ 是值，则它是数值，等于 $0$ 时用 E-PredZero，形如 $succ nv'$ 时用 E-PredSucc． T-IsZero 的情形与 T-Pred 相同，分别用 E-IsZero、E-IsZeroZero、E-IsZeroSucc．

∎

Example 3.2 进展 [progress]

2026-10-10
Glomzzz

采用类型与类型判断的类型规则和一步规约的求值规则．取良类型的项 $𝑡 = pred (if false then 0 else succ 0) : Nat$ ，跟着进展的证明走一遍．

$𝑡$ 的推导最后一步是 T-Pred，前提为 $if false then 0 else succ 0 : Nat$ ，对这个子项用归纳假设．子项的推导最后一步是 T-If，前提里有 $false : Bool$ ； $false$ 是值，由典范形式知它必为 $true$ 或 $false$ ，这里恰好是 $false$ ，于是用 E-IfFalse 得子项 $⟶ succ 0$ ．回到整项 $𝑡$ ，由于子项能规约，用 E-Pred 即得 $𝑡 ⟶ pred (succ 0)$ ．

这段证明在断定“能规约”的同时，直接构造出了这一步的推导．对 $pred (succ 0)$ 再用一次进展：子项 $succ 0$ 是值，由典范形式它是数值，且形如 $succ nv$ ，于是用 E-PredSucc 得到 $0$ ．对 $0$ 再用一次进展：它是值，停止．

对照 $succ true$ 受阻的原因与上面的证明：要让 $succ true$ 不受阻，要么 $true$ 能规约，要么 $true$ 是数值，两者都不成立．证明之所以没遇到这个麻烦，是因为 T-Succ 要求 $𝑡_{1} : Nat$ ，再经由典范形式把 $𝑡_{1}$ 限定为数值．类型系统正是在这里把坏程序挡在门外的．

4 保型

进展只能保证当前状态能运行，保型则让这个保证在运行后仍然可用．若修改 E-PredZero 为 $pred 0 ⟶ true$ ，原有类型规则仍会给 $succ (pred 0)$ 赋予类型 $Nat$ ，第一步也可以执行；但它会变成没有类型且受阻的 $succ true$ ．所以一次正确的类型检查必须能跨越每次运行时改写，不能“第一步安全就算安全”．编译器的优化、解释器的执行规则也要维持相应的不变量，否则即使前端检查器正确，后端仍能制造坏状态．

Theorem 4.1 保型 [preservation]

2026-10-10
Glomzzz

采用类型与类型判断的类型关系和一步规约的规约关系．若 $𝑡 : 𝑇$ 且 $𝑡 ⟶ 𝑡^{'}$ ，则 $𝑡^{'} : 𝑇$ ．

Proof.

对 $𝑡 ⟶ 𝑡^{'}$ 作规则归纳（规则归纳法），对 $𝑇$ 一般化．每个情形先对 $𝑡 : 𝑇$ 使用反演．

对 E-IfTrue， $𝑡 = if true then 𝑡_{2} else 𝑡_{3}$ ， $𝑡^{'} = 𝑡_{2}$ ，反演直接得 $𝑡_{2} : 𝑇$ ；E-IfFalse 对称，反演得 $𝑡_{3} : 𝑇$ ．对 E-If， $𝑡^{'} = if 𝑡_{1}^{'} then 𝑡_{2} else 𝑡_{3}$ ，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ；反演得 $𝑡_{1} : Bool$ 、 $𝑡_{2} : 𝑇$ 、 $𝑡_{3} : 𝑇$ ，对前提用归纳假设（取类型为 $Bool$ ）得 $𝑡_{1}^{'} : Bool$ ，再用 T-If 即得结论．对 E-PredZero， $𝑡^{'} = 0$ ，反演得 $𝑇 = Nat$ ，用 T-Zero．对 E-PredSucc， $t = pred (succ nv)$ ， $t' = nv$ ，反演两次先得 $𝑇 = Nat$ 且 $succ nv : Nat$ ，再得 $nv : Nat$ ．对 E-IsZeroZero 与 E-IsZeroSucc， $𝑡^{'}$ 是 $true$ 或 $false$ ，反演得 $𝑇 = Bool$ ，用 T-True 或 T-False．对同余规则 E-Succ，反演得 $𝑇 = Nat$ 且 $𝑡_{1} : Nat$ ，归纳假设给出 $𝑡_{1}^{'} : Nat$ ，再用 T-Succ；E-Pred 同理，最后用 T-Pred；E-IsZero 反演得 $𝑇 = Bool$ 且 $𝑡_{1} : Nat$ ，归纳假设给出 $𝑡_{1}^{'} : Nat$ ，最后用 T-IsZero．

∎

Example 4.2 保型 [preservation]

2026-10-10
Glomzzz

对多步规约到值的规约链，按类型与类型判断在每一项旁边写上类型．规约关系使用一步规约，保型性质及其证明见保型：

$\begin{matrix} if (iszero (pred (succ 0))) then succ 0 else 0 & : Nat \\ ⟶ & if (iszero 0) then succ 0 else 0 & : Nat \\ ⟶ & if true then succ 0 else 0 & : Nat \\ ⟶ & succ 0 & : Nat \end{matrix}$

类型始终是 $Nat$ ．以第一步为例看保型的证明怎样工作：这一步的推导是 E-If，前提是 $iszero (pred (succ 0)) ⟶ iszero 0$ ．由反演对 $𝑡 : Nat$ 反演，得到条件 $: Bool$ 、两个分支 $: Nat$ ；对前提用归纳假设（取类型 $Bool$ ），得到 $iszero 0 : Bool$ ；两个分支原封不动，再用 T-If 拼回去，得到新项 $: Nat$ ．

注意项本身变了很多，从 $if$ 表达式变成了 $succ 0$ ，但类型这一静态描述一直成立．保型说的就是：运行不会让类型作出的保证失效．

Note 4.3 保型证明中对

𝑇

的一般化 [generalizing-the-type-in-preservation-proofs]

2026-10-10
Glomzzz

打开独立页面 →

5 合起来

下面的推论把“当前不受阻”和“下一项仍有类型”接成对任意有限运行前缀的保证．只证明进展、缺少保型，保证可能一步后失效；只证明保型、缺少进展，则起初就受阻的良类型项没有任何一步可走，保型的条件从未成立，不能排除它．这个推论保证的是本文定义的“不受阻”，不保证程序一定终止，也不保证业务逻辑正确，例如得到 $false$ 是否符合程序员的意图．

Corollary 5.1 类型安全 [type-safety]

2026-10-10
Glomzzz

由词项的集合、一步规约与类型与类型判断规定的布尔值与自然数语言满足类型安全：若 $𝑡 : 𝑇$ 且 $𝑡 ⟶^{*} 𝑡^{'}$ ，则 $𝑡^{'}$ 没有受阻．

Proof.

对 $𝑡 ⟶^{*} 𝑡^{'}$ 的步数归纳（多步规约的两条规则）．零步时 $𝑡^{'} = 𝑡$ ，直接有 $𝑡^{'} : 𝑇$ ；至少一步时 $𝑡 ⟶ 𝑡_{1}$ 且 $𝑡_{1} ⟶^{*} 𝑡^{'}$ ，由保型得 $𝑡_{1} : 𝑇$ ，再对 $𝑡_{1}$ 用归纳假设即可．

归纳给出的其实是更强的结论： $𝑡^{'} : 𝑇$ ．最后对 $𝑡^{'}$ 用进展：它是值或还能规约，总之不受阻．

∎

类型安全本身不保证终止，但规约使大小严格下降已经另外证明了本文每条规约链都有限．把它与进展、保型和确定性接起来，还能得到更完整的求值结论：每个良类型项都会到达唯一的同类型值．

Corollary 5.2 良类型项求值到唯一的同类型值 [well-typed-terms-evaluate-to-unique-values]

2026-10-10
Glomzzz

采用词项的集合的有限项、值与数值的值、多步规约的多步规约，以及类型与类型判断的类型规则．若 $𝑡 : 𝑇$ ，则存在唯一的值 $𝑣$ ，使得

$𝑡 ⟶^{*} 𝑣 且 𝑣 : 𝑇 .$

Proof.

存在性．从 $𝑡$ 出发，只要有后继就继续规约．由规约使大小严格下降，每步大小严格下降，规约链至多有 $size (𝑡) - 1$ 步，因而必能到达没有后继的项 $𝑢$ ．由保型对链长归纳，得 $𝑢 : 𝑇$ ．再用进展： $𝑢$ 是值或还能规约；后一种情况已经排除，所以 $𝑢$ 是具有类型 $𝑇$ 的值．

唯一性．设 $𝑡 ⟶^{*} 𝑣$ 且 $𝑡 ⟶^{*} 𝑤$ ，其中 $𝑣$ 、 $𝑤$ 都是值．对第一条链的长度归纳；归纳性质允许第二条链任意长．若第一条链有零步，则 $𝑡 = 𝑣$ ．由值不可规约， $𝑡$ 没有后继，因此第二条链也只能有零步， $𝑤 = 𝑡 = 𝑣$ ．若第一条链至少有一步，它形如 $𝑡 ⟶ 𝑡_{1} ⟶^{*} 𝑣$ ． $𝑡$ 能规约，由值不可规约知它不属于值；第二条链不能有零步，必形如 $𝑡 ⟶ 𝑡_{2} ⟶^{*} 𝑤$ ．由确定性得 $𝑡_{1} = 𝑡_{2}$ ．两条剩余链从同一项出发，第一条的长度更小，由归纳假设得 $𝑣 = 𝑤$ ．

∎

类型安全只排除受阻，不独自保证终止．这条推论还用到了另行证明的终止性与确定性；它针对上述未扩展语言，不能直接推广到含一般递归或其他求值规则的语言．

Remark 5.3 约定与必然 [convention-and-necessity]

2026-10-10
Glomzzz

打开独立页面 →

6 练习：类型安全

Exercises (4)

Exercise 5.1. 把进展与保型放到同一条链上

对

if (iszero (pred (succ 0))) then pred 0 else succ 0

写出规约链与每站类型．逐步说明进展在哪里提供后继，保型又怎样重建类型，并解释第一步内部用到的类型为何不都是整项的

Nat

．

Hint

每个中间项都为

Nat

；条件内部先保持

Nat

，外层

iszero

保持

Bool

，不能把这两个类型混成一个固定的

𝑇

．

Solution

$\begin{matrix} if (iszero (pred (succ 0))) then pred 0 else succ 0 & : Nat \\ ⟶ & if (iszero 0) then pred 0 else succ 0 & : Nat \\ ⟶ & if true then pred 0 else succ 0 & : Nat \\ ⟶ & pred 0 & : Nat \\ ⟶ & 0 & : Nat \end{matrix}$

四步依次用 E-If + E-IsZero + E-PredSucc，E-If + E-IsZeroZero， E-IfTrue，E-PredZero．每个非末项都展示了进展要求的一个后继，末项 $0$ 展示了“已经是值”的分支．

第一步内层 $pred (succ 0)$ 从 $Nat$ 保持为 $0 : Nat$ ， T-IsZero 重建条件的 $Bool$ ，T-If 再和两个 $Nat$ 分支重建整项的 $Nat$ ．第二步条件变成 $true : Bool$ ，分支不变；第三步选出的 $pred 0$ 本来就在 T-If 的前提里具有 $Nat$ ；第四步由 T-Zero 得 $0 : Nat$ ．这样逐步重建推导，才交代清楚了类型保持的原因．

Exercise 5.2. 扩展：进展与保型的配合

分别考虑两种修改：删除 E-PredZero，或者把它改成

pred 0 ⟶ true

，其余求值与类型规则都保留．指出每种修改破坏进展还是保型、另一条是否仍成立，并用具体项说明只保留其中一条会漏掉什么．

Hint

分别修改，不要把两种修改混到同一门语言里．保型只对实际存在的规约步骤作保证．

Solution

删除 E-PredZero 而保留其他规则时， $pred 0 : Nat$ 既非值也没有后继，进展失效．但剩下的每一步仍是原语言合法的步骤，因此仍保型．保型无法排除一个根本没有步骤的坏终点．

将 E-PredZero 改为 $pred 0 ⟶ true$ 时， $pred 0 : Nat$ 走到 $true : Bool$ ，保型失效．原来的进展证明仍能为每个良类型非值找到一步， T-Pred 的零参数情形只是把后继换了一个；但它不保证后继仍良类型．

例如 $succ (pred 0) : Nat$ 在第二种修改下走到受阻的 $succ true$ ．所以“现在有下一步”与“类型保证能传到下一项”必须一起使用，见类型安全．

Exercise 5.3. 保型的逆命题

判断命题“若

𝑡 ⟶ 𝑡^{'}

且

𝑡^{'} : 𝑇

，则

𝑡 : 𝑇

”是否与保型等价；若不等价，给出原语言中的一步反例，并说明它与保型并无矛盾．

Hint

从“分支类型不同，但运行选中一个正常分支”的项开始寻找．

Solution

不成立．取 $𝑡 = if true then 0 else false$ ， E-IfTrue 给出 $𝑡 ⟶ 0$ ，且 $0 : Nat$ ，但 $𝑡$ 没有类型： T-If 要求两个分支具有同一类型，而 $0$ 与 $false$ 的类型不同．

这不违反保型，因为保型的前提是起点已有类型．从一个正常的终点倒推起点有类型，相当于把单向蕴涵改成了逆命题，类型系统是保守的已经提醒过不能这样用．

Exercise 5.4. 扩展：不受阻，仍然可以永远运行

只将 E-PredZero 改成

pred 0 ⟶ pred 0

，其余规则不变．分析从

pred 0

出发的运行是否受阻、是否保型、是否终止；指出进展与保型的证明只需调整哪个情形，以及“每步让项变小”的论证在哪一步失效．

Hint

把 E-PredZero 改成自循环步骤，但不保留它原来规约到

0

的版本．检查下一步是否存在、类型是否改变、大小是否下降．

Solution

新规则是 $pred 0 ⟶ pred 0$ ． $pred 0 : Nat$ 仍非值，始终有下一步，所以没有受阻；每一步又回到同一个具有 $Nat$ 的项，因此这条链一直保持类型，却永不结束．

原进展证明的 T-Pred 零参数情形仍有后继；原保型证明的 E-PredZero 情形改为“结果就是起点，已有 $Nat$ ”．其他情形不变，所以这门修改后的语言仍可证明进展、保型与不受阻的类型安全．

但大小始终为 $2$ ，原语言“每一步严格变小”的论证不能再用，求值循环也不能再保证停止．类型安全没有承诺终止；要证明终止，还需要另外的下降度量或其他证明．

. 类型安全：典范形式、进展与保型

References

Backlinks