.
总结
. 总结
回顾从抽象语法、小步语义到类型安全与检查器可靠性的定义、归纳与证明链条．
全文走过的路，按前后的依赖关系首尾相接． 从自然语言在结构、完备、量词、自指、可检查性上的五个弊端（ 结构歧义 至 Berry 悖论 ）出发，我们先引入对象语言与元语言的分层（ 对象语言与元语言 ）； 接着用“满足封闭条件的最小集合”定义项（ 词项的集合 ），由“最小”直接导出结构归纳（ 结构归纳原理 ）； 再用同样的最小性定义小步语义的转移关系（ 一步规约 ），得到规则归纳法（ 规则归纳法 ），进而证明确定性（ 确定性 ）以及大小严格下降带来的终止性（ 规约使大小严格下降 ）．
在此基础上，我们用推导规则定义类型关系及其可推导的类型判断（ 类型与类型判断 ），借助语法导向证明反演（ 反演 ）、类型唯一与典范形式； 再把进展与保型合起来，得到类型安全，即本文意义下的类型健全性（ 类型安全 ），并结合另行证明的终止性与确定性，推出良类型项求值到唯一的同类型值（ 良类型项求值到唯一的同类型值 ）． 最后，证明检查器相对规则可靠且完备，把“检查器接受”与“运行不受阻”接成完整的端到端结论（ 检查器接受的程序不会受阻 ）．
贯穿始终的方法只有一个： 先把东西定义成满足某些规则的最小对象，再沿着这些规则归纳． 语言变大以后，规则会变多，证明会变长，但这个方法不变． 它在数学和逻辑史上的来历，见 “最小 + 归纳”的历史 ．
2 延伸阅读
本系列的布尔值与自然数语言、规则名称与证明主线以 Types and Programming Languages（TAPL）为基础． 术语译名以香蕉空间的条目为准， 香蕉空间尚未收录的术语参考下面两篇中文译文； 全部术语对照见 术语对照 ． 参考译文不意味着把不同模型的规则或结论直接移植到本文．
Benjamin C. Pierce 的 Types and Programming Languages（《类型和程序设计语言》）第 2 章讲归纳定义与归纳法，第 3、8 章就是本文这门语言，规则名沿用了它的写法． Benjamin C. Pierce 等人的 Software Foundations（《软件基础》）在 Coq（现名 Rocq）里从零开始讲归纳证明； 第二卷 Programming Language Foundations 的
Types
Types
一章给出相近算术语言的形式化定义，讲解进展、保型和类型安全，并留下相关机械化证明练习（公开代码中的
Admitted
Admitted
留作待读者补全的练习，该章也不涉及本文的 Rust 实现）．
进展加保型这种证明方式出自 Andrew K. Wright 与 Matthias Felleisen 1994 年发表于 Information and Computation 的论文 A Syntactic Approach to Type Soundness． Robert Harper 的 Practical Foundations for Programming Languages（《编程语言的实用基础》）第 1、2 章对“抽象语法”和“归纳定义”的处理比 TAPL 更细致．
中文入门文章可读 Chuigda Whitegive 翻译的两篇： Graham Hutton 著的《程序语言语义学：数数手指一二三》用整数与加法语言比较指称语义、小步语义、语境语义和大步语义，讲解结构归纳法与规则归纳法，并进一步推演抽象机； Alexis King 著的《如何阅读类型系统符号》说明文法、词项与类型、类型判断、公理和推导规则，以及语境、附加条件和类型判断的算法解释．