编程语言理论与类型系统入门

附录C：自检问题

本附录不是“考试题集”，而是配合正文使用的阶段性自检清单。它的目标不是考你是否记住了每个公式，而是帮助你判断：

• 哪些概念你已经真正理解了；
• 哪些地方只是“看着眼熟”，但还不能独立推导；
• 下一步应该回看哪一章、补哪一类练习。

如何使用这份自检题？

建议把题目按三种层次来使用：

一、基础掌握

这类问题主要检查你是否掌握了每章的核心定义、规则和最基本例子。
如果这些题做不出来，说明你还不适合直接进入后续章节。

二、推导与分析

这类问题要求你手动做自由变量计算、替换、类型推导、约束生成、合一等操作。
如果这些题做不出来，通常表示你已经“知道这个概念是什么”，但还没有真正会用。

三、综合理解

这类问题要求你把一章内部的多个概念联系起来，或者把不同章节之间的主线串起来。
如果这些题做不出来，不一定说明你前面没学会，更可能说明你还没把本教程的整体结构建立起来。

如何把本附录和其他附录一起用？

本附录最适合和另外两个附录一起配合：

• 附录A：术语表
  • 当你卡在“概念分不清”时先查这里；
  • 例如：值 / 范式 / 卡住、类型检查 / 类型推断、协变 / 逆变。
• 附录B：符号速查表
  • 当你卡在“符号看不顺”时先查这里；
  • 例如：Γ ⊢ t : T、→、∀、<:、⊸。
• 本附录C：自检问题
  • 用来判断你是否已经能真正自己做推导、计算和解释。

也就是说，最常见的排错顺序通常是：

1. 先看正文对应章节；
2. 再查附录A确认术语；
3. 再查附录B确认符号；
4. 最后回到本附录重新做题。

如果你做题时总在术语或记号上卡住，优先回查附录A、附录B，而不是立刻回正文大段重读。
很多时候，问题并不是“整章没看懂”，而只是某个术语边界或某个记号读法还没稳定下来。

建议的使用节奏

• 每学完一章后，先做该章的“基础掌握”题。
• 如果能顺利完成，再做“推导与分析”题。
• 每学完两到三章后，回头做一次前面章节的“综合理解”题，检查自己是否还能把主线串起来。
• 如果你是第二遍阅读本教程，建议直接优先做“推导与分析”和“综合理解”部分。

建议的做题方式

为了让这份自检题真正起作用，建议尽量避免“看一眼题目，觉得自己会了”这种浏览式做法。更有效的方式通常是：

1. 先闭卷回答
   • 不看正文、不看附录，先尝试自己写出定义、规则或推导。
2. 再对照正文与附录
   • 检查自己错在：
     • 术语没分清；
     • 记号没读准；
     • 规则会背但不会用；
     • 还是跨章节主线没串起来。
3. 最后做一次最小复现
   • 例如：
     • 再手算一次替换；
     • 再手画一次推导树；
     • 再手做一次合一；
     • 再手判断一次环境分裂。

如果你能做到“闭卷写出一个最小例子”，通常就说明这个知识点已经开始内化了。

第1章 数学基础

若这一章做题不顺，建议先回看第 1 章正文；若你对“关系 / 推导规则 / 结构归纳 / 推导归纳”这些词本身已经有点混淆，再配合附录A对应条目一起看。

基础掌握

1. 什么是二元关系？它与集合之间是什么关系？
2. 什么是前序、偏序、等价关系？它们分别需要哪些性质？
3. 归纳定义和归纳法各解决什么问题？
4. 推导规则的一般形式是什么？什么是公理？

推导与分析

5. 设 $A=\{1,2,3,4\}$，$B=\{3,4,5,6\}$，计算：

   • $A\cup B$
   • $A\cap B$
   • $A\setminus B$
   • $A\times B$

6. 用归纳定义的方式定义“合法括号串”。

7. 用推导规则定义自然数上的“小于等于”关系，并尝试推出： $$2\le 4$$

8. 用结构归纳法证明：每个算术表达式的大小（节点数）至少为 1。

9. 设有推导规则： $$\frac{}{0<S(n)}\frac{n<m}{S(n)<S(m)}$$ 尝试手工构造一个推出 $$1<3$$ 的推导树。

综合理解

10. 为什么说后续的语法定义、类型规则和类型安全证明，都离不开“归纳定义 + 推导规则 + 归纳法”这三件工具？

第2章 形式文法与 BNF

若这一章做题不顺，建议先回看第 2 章正文；若你对“终结符 / 非终结符 / 具体语法 / 抽象语法 / AST”这些概念已经混在一起，再配合附录A与附录B一起看。

基础掌握

11. 形式文法想解决什么问题？为什么自然语言描述语法不够？
12. BNF 中的 ::= 和 | 分别表示什么？
13. 什么是终结符？什么是非终结符？
14. 具体语法和抽象语法有什么区别？

推导与分析

15. 用 BNF 定义一个简单的布尔表达式语言，包含：

• true
• false
• not
• and
• or

并体现：

• not 优先级高于 and
• and 优先级高于 or

16. 用你定义的文法推导字符串： $$trueand(falseortrue)$$

17. 为表达式 $$1+2\ast 3$$ 画出对应的抽象语法树（AST）。

18. 试着说明：为什么后续章节里写成 $$t::=\cdots$$ 这样的生成式时，通常更应理解为抽象语法对象的归纳定义，而不是完整源代码语法？

综合理解

19. 为什么说类型系统主要工作在抽象语法层，而不是源代码表面的具体写法上？

第3章 Lambda 演算基础

若这一章做题不顺，建议先回看第 3 章正文；若你对 FV(t)、[x ↦ s]t、\equiv_\alpha 这些记号不熟，先查附录B；若你对“自由变量 / 绑定变量 / α-等价 / 替换 / 新鲜变量”这些术语分不清，再查附录A。

基础掌握

20. Lambda 演算（Lambda Calculus）的三种基本构造是什么？
21. 什么是绑定变量（bound variable）？什么是自由变量（free variable）？
22. 什么叫 α-等价（alpha-equivalence）？
23. 替换 $[x\mapsto s]t$ 的直觉含义是什么？
24. 为什么替换时必须避免变量捕获（variable capture）？

推导与分析

25. 计算下列项的自由变量集合：

• $\lambda x.xyz$
• $(\lambda x.x)y$
• $\lambda x.\lambda y.xz$

26. 判断下列各对项是否 α-等价，并说明理由：

• $\lambda x.x$ 与 $\lambda y.y$
• $\lambda x.\lambda y.x$ 与 $\lambda a.\lambda b.a$
• $\lambda x.y$ 与 $\lambda y.y$

27. 计算下列替换，并写出关键步骤：

• $[x\mapsto y](\lambda z.xz)$
• $[x\mapsto y](\lambda y.x)$
• $[x\mapsto \lambda z.zw](\lambda y.xy)$，其中 $w$ 是自由变量

28. 试着解释：为什么“新鲜变量”不是“宇宙中从未出现过的变量”，而是“对当前替换步骤足够新、不会引发冲突的变量”？

综合理解

29. 为什么说 α-等价和避免捕获的替换，是后面 β-归约与类型系统形式化的基础？

第4章 Lambda 演算中的计算

若这一章做题不顺，建议先回看第 4 章正文；若你对“β-归约 / redex / 范式 / 发散 / 传名调用 / 传值调用 / 小步语义 / 大步语义”这些术语或记号不稳，先配合附录A、附录B一起查。

基础掌握

30. 什么是 β-归约（beta-reduction）？
31. 什么是可归约表达式（redex）？
32. 什么是范式（normal form）？
33. 传名调用（call-by-name）和传值调用（call-by-value）的区别是什么？
34. 小步语义（small-step semantics）和大步语义（big-step semantics）分别强调什么？

推导与分析

35. 逐步归约下列项：

• $(\lambda x.x)y$
• $(\lambda x.\lambda y.x)ab$
• $(\lambda f.\lambda x.fx)(\lambda y.y)z$

36. 解释为什么下面这个归约不能直接做“无脑替换”： $$(\lambda x.\lambda y.x)y$$ 并给出正确结果。

37. 对下列项分别先归约外层和先归约内层： $$(\lambda x.a)((\lambda y.b)c)$$ 观察它们是否会得到一致结果。

38. 比较下列项在传名调用和传值调用下的行为： $$(\lambda x.a)\Omega \Omega =(\lambda x.xx)(\lambda x.xx)$$ 说明为什么两种策略的终止性不同。

39. 试着说明：为什么 4.1–4.6 节里可以先用开放项建立策略直觉，而 4.8 节开始又要切换到更严格的小步语义规则？

综合理解

40. Church–Rosser 定理保证了什么？
41. 为什么本章主要解决“程序如何计算”，而“程序为什么不会卡住”要等到下一章才真正形式化？

第5章 类型系统核心概念

若这一章做题不顺，建议先回看第 5 章正文；若你对 Γ ⊢ t : T、进展性、保持性、类型安全、替换引理这些概念不稳，建议同时回查附录A和附录B。

基础掌握

42. 类型系统在这一章里试图排除的核心坏状态是什么？
43. 类型判断 $$\Gamma ⊢t:T$$ 的含义是什么？
44. 本章对象语言为什么更准确地说是“带布尔值与条件表达式的 STLC 扩展”？
45. 什么是进展性（progress）？
46. 什么是保持性（preservation）？

推导与分析

47. 构造推导树，证明： $$f:\text{Bool}\to \text{Bool},x:\text{Bool}⊢fx:\text{Bool}$$

48. 说明为什么下面这个项无法通过类型检查： $$\text{true}(\lambda x:\text{Bool}.x)$$

49. 构造推导树，证明： $$⊢\lambda x:\text{Bool}.\text{if }x\text{ then false else true}:\text{Bool}\to \text{Bool}$$

50. 用自然语言解释替换引理在保持性证明中的作用。

51. 试着区分：

• 声明式类型规则在回答什么问题？
• 语法制导的类型检查过程又在回答什么问题？

综合理解

52. 为什么“类型安全 = 进展性 + 保持性”？
53. 为什么“良类型程序不会出错”不能被理解成“良类型程序一定正确”？

第6章 一阶类型系统：基本类型构造

若这一章做题不顺，建议先回看第 6 章正文；若你对积类型、和类型、记录类型、递归类型、fold / unfold、Ref(T) 这些构造已经混在一起，先查附录A与附录B，再回来做题。

基础掌握

54. 什么是一阶类型系统（first-order type system）？这里的“一阶”主要排除了什么能力？
55. Bool、Nat、Unit 的直觉含义分别是什么？
56. 什么是积类型（product type）？什么是和类型（sum type）？
57. 什么是记录类型（record type）？它与积类型是什么关系？
58. 什么是递归类型（recursive type）？为什么它对列表、树这类结构是必要的？
59. 什么是引用类型 Ref(T)？

推导与分析

60. 解释为什么 if t1 then t2 else t3 的两个分支必须有相同类型。

61. 写出一个 Bool × Nat 类型值的例子，并说明如何分别取出它的两个分量。

62. 用自然语言解释类型： $$\text{Nat}+\text{Bool}$$ 中的值可能长什么样。

63. 解释为什么列表类型可以写成： $$\mu L.\text{Unit}+(T\times L)$$

64. 说明为什么引入 Ref(T) 之后，类型安全证明需要额外跟踪存储的类型信息。

65. 试着说明：为什么第 6 章允许显式写出递归类型 \mu X.T，而这并不等于说第 9 章的 HM 合一就会允许任意“无限类型”自动出现？

综合理解

66. 为什么说一阶类型系统的核心任务，是让类型系统能够描述常见的数据形态，而不仅仅是函数？

第7章 二阶类型系统：多态与抽象

若这一章做题不顺，建议先回看第 7 章正文；若你对 ∀、∃、ΛX.t、t[T]、参数化多态、存在类型、打包 / 拆包这些概念不稳，先配合附录A与附录B一起看。

基础掌握

67. 为什么一阶类型系统无法自然表达“对任意类型都成立的恒等函数”？
68. 什么是参数化多态（parametric polymorphism）？
69. System F 比普通 STLC 多了哪两类核心构造？
70. 全称类型 $\forall X.T$ 的直觉含义是什么？
71. 存在类型（existential type） $\exists X.T$ 的直觉含义是什么？
72. 什么是类型算子（type operator）？

推导与分析

73. 写出多态恒等函数的 System F 项，并说明它为什么具有类型： $$\forall X.X\to X$$

74. 解释为什么： $$id[\text{Bool}]:\text{Bool}\to \text{Bool}$$ 和 $$id[\text{Nat}]:\text{Nat}\to \text{Nat}$$ 可以看作同一个多态项的不同实例化。

75. 比较：

• $\forall X.X\to X$
• $\exists X.X\to X$

并说明它们在直觉上的区别。

76. 用自然语言解释为什么存在类型可以表达“隐藏实现、暴露接口”。

77. 试着说明：为什么第 7 章对象语言中的 ∀X.T 与 ΛX.t，不应直接和第 9 章 HM 环境中的类型方案 ∀α.T 混为一谈？

综合理解

78. 为什么说二阶类型系统让我们不仅能给项分类，还能对类型本身做抽象？
79. 为什么参数化多态与存在类型一起构成了类型化抽象的重要基础？

第8章 子类型

若这一章做题不顺，建议先回看第 8 章正文；若你对 S <: T、T-Sub、安全替换、协变 / 逆变 / 不变这些概念仍然摇摆，先查附录A和附录B，再回来重新看函数子类型的方向。

基础掌握

80. 子类型（subtyping）关系 $$S<:T$$ 的直觉含义是什么？
81. 什么是安全替换原则？
82. 为什么 T-Sub（subsumption）是子类型系统的关键规则？
83. 记录宽度子类型化（width subtyping）是什么意思？
84. 为什么函数参数逆变（contravariance），而返回值协变（covariance）？

推导与分析

85. 解释为什么下面的子类型关系成立： $$\{name:\text{String},age:\text{Nat}\}<:\{name:\text{String}\}$$

86. 给出一个具体反例，说明如果函数参数按协变处理，会产生什么类型安全问题。

87. 设有： $$Cat<:Animal$$ 讨论下列哪一个关系应成立，并说明理由：

• $Animal\to Cat<:Animal\to Animal$
• $Cat\to Cat<:Animal\to Cat$
• $Animal\to Animal<:Cat\to Animal$

88. 用自然语言解释为什么引用类型通常不能简单协变或逆变。

89. 试着说明：为什么本章主要处理的是“可安全提升”的 <: 关系，而不是第 9 章里那种“必须相等”的类型等式与合一问题？

综合理解

90. 为什么本章的真正主线不是“列举哪些类型有子类型关系”，而是“如何通过 T-Sub 把子类型接入类型系统”？

第9章 类型推断

若这一章做题不顺，建议先回看第 9 章正文；如果你已经把“替换”“类型方案”“泛化”“实例化”“合一”“occur check”混在一起，最好同时回查附录A与附录B，并顺手对照第 7 章重新看“显式多态”和“HM 推断”的区别。

基础掌握

91. 类型推断和类型检查的区别是什么？
92. 什么是 Curry 风格（Curry-style）项？
93. 类型推断为什么可以分解成“生成约束（constraint generation）+ 求解约束”？
94. 什么是合一（unification）？
95. 什么是 occur check？
96. 什么是 let 多态（let polymorphism）？

推导与分析

97. 推断下列项的最一般类型：

• $\lambda x.x$
• $\lambda f.\lambda x.fx$
• $\lambda x.\lambda y.x$

98. 对项 $$\lambda x.xx$$ 手工生成约束，并说明为什么合一失败。

99. 对约束组 $$\alpha \to \alpha =\text{Bool}\to \beta$$ 手工执行合一步骤，写出每一步的替换传播与最终结果。

100. 解释为什么下面的表达式在 HM 中可以通过：

let id = fun x -> x in (id true, id 0)

101. 解释为什么下面的表达式在标准 HM 中通常不能通过：

fun id -> (id true, id 0)

102. 试着说明：为什么第 9 章里对 \lambda f.\lambda x.f x 的推断，最先得到的是一个最一般单态类型；而“全称量化后的类型方案”要到顶层或 let 绑定语境里才最自然？

综合理解

103. 为什么函数类型的合一不能简单把两个子问题的结果做“并集”，而必须传播并组合替换？
104. 为什么只有 let 绑定触发泛化，而普通函数参数通常保持单态？
105. 为什么 HM 的 let 多态不应被理解成“完整 System F 的自动推断版”？

第10章 子结构类型系统

若这一章做题不顺，建议先回看第 10 章正文；若你对“结构规则 / 环境分裂 / 线性函数 / 仿射资源 / 会话类型”这些概念还没有形成稳定图景，最好同时回查附录A与附录B，并顺手回看第 6 章引用类型、第 8 章变化方向的相关部分。

基础掌握

106. 什么是结构规则？
107. 交换、弱化、收缩分别表达什么？
108. 线性、仿射、相关、有序类型系统分别限制了什么？
109. 什么是环境分裂？
110. 为什么子结构类型系统不仅关心“值是什么”，还关心“值怎样被使用”？

推导与分析

111. 解释为什么“允许收缩”会让资源管理变得危险。
112. 说明仿射类型和线性类型的区别，并各举一个更适合它们的资源场景。
113. 为什么环境分裂是线性函数应用规则中的关键机制？
114. 设想一个“先发送请求，再接收响应”的通信协议，说明为什么单纯的线性使用还不够，还需要顺序约束。
115. 解释为什么不能简单说“Rust 就是线性类型系统”或“Rust 就是仿射类型系统”。
116. 试着比较：

• 第 5 章主要关心“项是否良类型”；
• 第 10 章进一步关心“变量能否被丢弃、复制或乱序使用”。

说明这两类约束的层次差别。

综合理解

117. 常规类型系统为什么会把“变量可自由复制与丢弃”当成默认前提？
118. 为什么子结构类型系统可以看作一种把“资源使用纪律”纳入类型系统的方式？

跨章节综合题

下面这些问题适合在你完成正文一遍阅读后再做。

主线回顾

119. 用自己的话说明本教程的大主线：

• 语法定义了什么？
• 语义定义了什么？
• 类型系统定义了什么？
• 元理论又说明了什么？

120. 为什么要先学 Lambda 演算，再学类型系统？
121. 为什么类型安全证明离不开第三章的替换和第四章的操作语义？

对比与联系

122. 比较下列几组概念：

• α-等价 vs β-归约
• 值 vs 范式
• 类型检查 vs 类型推断
• 参数化多态 vs 子类型
• 线性类型 vs 仿射类型

123. 为什么说：

• 第五章关心“程序为什么不会卡住”
• 第九章关心“程序员不写注解时系统怎么恢复类型”
• 第十章则进一步关心“值应该怎样被使用”

124. 试着说明下列两组“全称量化”为什么不能简单混为一谈：

• 第 7 章中的 ∀X.T
• 第 9 章 HM 环境中的类型方案（type scheme） ∀α.T

125. 试着说明下列两组“递归 / 无限”为什么也不能简单混为一谈：

• 第 6 章中的显式递归类型 μX.T
• 第 9 章 occur check 所阻止的无限类型（infinite type）

更进一步的反思

126. 为什么类型系统必须是“保守的近似”，而不能精确分析程序所有语义行为？
127. 为什么“表达力更强”往往会和“推断更难、实现更复杂”同时出现？
128. 如果让你用一句话分别概括第 3–10 章各章的核心贡献，你会怎么写？

使用这份自检题时的一个提醒

如果你发现自己：

• 能复述定义；
• 但做不出推导；
• 或者能做局部推导，但说不清章节主线；

这都很正常。它通常说明你正处在“从看懂走向会用”的阶段。

这份附录的作用，不是让你因为不会而沮丧，而是帮你定位：

• 是定义没有真正理解；
• 还是规则不会操作；
• 还是跨章节的主线还没有建立起来。

只要你能据此回到对应章节，有针对性地重做例子和练习，这份自检题就达到了它的目的。

如果你想把这份附录用得更有效，可以把每次做题后的结果简单记成三类：

• 会复述，但不会算
• 会算局部，但不会串主线
• 已经能闭卷做最小例子

这样你在第二轮、第三轮回看本教程时，会更容易判断自己下一步该补哪一类能力。