附录B：符号速查表

本附录是一个参考型速查表，适合在阅读正文时随时回查。
它的目标不是替代正文解释，而是帮助你快速确认：

某个符号怎么读；
它大致表示什么；
它在本教程的哪类语境中出现。

使用方式建议：

第一次阅读正文时，不必强行记住全部符号；

遇到不熟悉的记号时，再回到这里查；

若你想看更完整的术语解释，请配合附录A“术语表”一起使用。

阅读提醒：

同一个符号在不同章节里，可能处在不同层级；

例如第 7 章的 ∀X.T 是对象语言中的全称类型，而第 9 章的 ∀α.T 更常出现在 HM 风格环境中的类型方案（type scheme）；

又例如第 7 章的 X, Y 通常表示显式多态系统中的类型变量，而第 9 章的 α, β, γ 通常表示推断过程中临时生成的未知类型占位符。

一、逻辑与判断相关记号

记号	常见读法	含义	常见语境
$\land$	且	逻辑合取（and）	命题逻辑、性质并列
$\lor$	或	逻辑析取（or）	命题逻辑、分类讨论
$\Rightarrow$	蕴含 / 如果……那么……	逻辑蕴含	规则描述、性质定义
$\forall$	对所有 / 任意	全称量词	多态、数学定义
$\exists$	存在	存在量词	存在类型、数学定义
$⊢$	可推出 / 可判断为	在某套规则系统中可以推出某结论	类型判断、推导系统
$Γ ⊢ t : T$	在环境 $Γ$ 下， $t$ 的类型是 $T$	类型判断	第5章及以后
$Γ (x)$	环境中查找 $x$ 的类型	环境查找结果	类型规则

说明：
$\vdash$ 不应简单理解成普通语言里的“所以”。它通常表示：
在某个形式系统的规则之下，可以推出右边的判断。

二、Lambda 演算相关记号

记号	常见读法	含义	常见语境
$λ x . t$	lambda x 点 t	函数抽象（函数定义）	第3章起
$t_{1} t_{2}$	把 $t_{1}$ 应用于 $t_{2}$	函数应用	第3章起
$F V (t)$	t 的自由变量集合	自由变量集合	第3章
$[x \mapsto s] t$	把 $t$ 中的 $x$ 替换为 $s$	项替换	第3章、第4章
$\equiv_{α}$	α-等价	绑定变量重命名后的等价	第3章
$⟶_{β}$	β-归约到	一步 β-归约	第4章
$⟶$	归约到 / 一步归约到	一步计算关系	第4章起
$⟶^{*}$	多步归约到	零步或多步归约	第4章起
$t ⇓ v$	t 求值为 v	大步语义中的求值关系	第4章
$Ω$	Omega	经典发散项	第4章
redex	可归约表达式	形如 $(λ x . t) s$ 的可归约子项或位置	第4章
$η$	eta	常用于 η-归约或 η-等价的记号	第4章（补充概念）

说明：
$[x \mapsto s]t$`` 中的 $\mapsto$ ` 在这里读作“替换为”最自然；
但在别的上下文里，它也可能只是一般意义上的“映射到”。

三、类型系统相关记号

记号	常见读法	含义	常见语境
$T, U, S$	类型元变量 / 类型占位记号	表示任意类型的占位符，不是对象语言里的类型变量	全书
$A, B$	基础类型或一般类型名	视上下文而定	第5章起
$T_1 \to T_2$	从 $T_1$ 到 $T_2$	函数类型	第5章起
$\text{Bool}$	Bool	布尔类型	第5章起
$\text{Nat}$	Nat	自然数类型	第5章起
$\text{Unit}$	Unit	单位类型	第6章
$T_1 \times T_2$	积类型 / 乘积类型	同时包含两个部分的类型	第6章
$T_1 + T_2$	和类型 / 和	二选一的类型	第6章
${l_1:T_1,\dots,l_n:T_n}$	记录类型	带字段名的类型	第6章、第8章
$\mu X.T$	mu X 点 T	递归类型	第6章
$\text{fold}(t)$	fold t	把展开后的递归结构重新包回递归类型	第6章
$\text{unfold}(t)$	unfold t	把递归类型打开一层	第6章
$\text{Ref}(T)$	Ref of T / T 的引用类型	可变引用类型	第6章
$\forall X.T$	对所有类型 $X$，$T$	全称类型	第7章
$\exists X.T$	存在某个类型 $X$ 使得 $T$	存在类型	第7章
$\Lambda X.t$	大 Lambda X 点 t	类型抽象	第7章
$t[T]$	t 作用于类型 T	类型应用	第7章
$\text{pack}$	pack	存在类型中的打包（packing）构造	第7章
$\text{unpack}$	unpack	存在类型中的拆包（unpacking）构造	第7章
$S <: T$	S 是 T 的子类型	子类型关系	第8章

说明：

T1→T2 中的箭头表示函数类型，不是程序执行步骤。

S<:T 表示“S 可以安全地用在需要 T 的地方”。

四、类型推断与合一相关记号

记号	常见读法	含义	常见语境
$\alpha, \beta, \gamma$	类型变量	推断中的未知类型占位符	第9章
$\sigma$	替换 sigma	把类型变量映射为类型的替换	第9章
$T\text{-}Sub$	T-Sub / subsumption	把已有类型提升到其超类型的类型规则	第8章
$\sigma(T)$	把替换 $\sigma$ 作用到类型 $T$ 上	替换作用结果	第9章
$\sigma_2 \circ \sigma_1$	替换组合	先做 $\sigma_1$，再做 $\sigma_2$	第9章
$\text{unify}(\cdots)$	合一	求解类型等式	第9章
$\forall \alpha.T$	对类型变量 $\alpha$ 全称量化	HM 风格类型方案中的量化	第9章
$\text{Gen}(\Gamma, T)$	在环境 $\Gamma$ 下泛化 $T$	泛化操作	第9章
$\text{Inst}(Sch)$	实例化一个类型方案	把类型方案中的量化变量替换为新鲜类型实例	第9章
$Sch$	scheme / 类型方案	HM 风格环境中记录的一族类型	第9章

说明：
在第9章里，$\alpha,\beta,\gamma$ 通常不表示“真实语言中的泛型参数”，
而是推断算法中临时生成的未知类型占位符。

五、子结构类型系统相关记号

记号	常见读法	含义	常见语境
$\text{lin}$	linear	线性限定符	第10章
$\text{un}$	unrestricted	无限制限定符	第10章
$A \multimap B$	线性函数类型	线性地消耗一个 $A$，产生一个 $B$	第10章
$\Gamma_1 \circ \Gamma_2$	环境分裂 / 环境组合	表示线性系统中的环境拆分或对应组合	第10章
Exchange	交换规则	允许调整环境中假设的顺序	第10章
Weakening	弱化规则	允许引入未使用的变量假设	第10章
Contraction	收缩规则	允许重复使用同一假设	第10章

本教程约定：
Γ1∘Γ2 不是所有教材里都统一采用的通用记号。
在本教程中，它专门表示：

两个环境之间的线性分裂 / 组合关系；

直觉上可理解为“把资源分给左右两个子推导”。

阅读第10章时，请始终按这个约定理解它。

六、正文中常见的元变量约定

这些不是“语言里的变量”，而是作者在讲解时常用的元变量。

记号	常见含义
$t, s, u$	项（term）
$x, y, z$	程序变量
$v$	值（value）
$T, U, S$	类型（元变量）
$X, Y$	类型变量（多见于第 7 章显式多态系统）
$\alpha, \beta, \gamma$	推断中的未知类型变量（多见于第 9 章）
$\Gamma$	类型环境 / 上下文
$\sigma$	替换
$Sch$	类型方案（type scheme）
$e$	表达式（有时用于一般表达式语言）

提醒：
元变量是“讲解语言”的记号，不是目标语言本身的一部分。
例如 t::=x∣λx.t∣t t 里的 t 是在描述“任意项”的元变量，不是程序里真的有个变量叫 t。

特别注意：

第 7 章里的 X,Y 通常表示对象语言类型中的类型变量；

第 9 章里的 alpha,beta,gamma 通常表示推断算法临时生成的未知类型占位符；

两者都可被叫作“类型变量”，但层级和用途并不相同。

七、容易混淆的符号对照

记号	不要和什么混淆	区别
$T_1 \to T_2$	$\longrightarrow$	前者是函数类型，后者是归约关系
$\lambda x.t$	$\Lambda X.t$	前者是值层面抽象，后者是类型层面抽象
$[x \mapsto s]t$	$\sigma(T)$	前者是项替换，后者通常是类型替换 / 替换作用
$\equiv_\alpha$	$\longrightarrow_\beta$	前者是等价关系，后者是一步归约关系
$\forall X.T$	$\forall \alpha.T$	前者多见于第 7 章的显式多态对象语言，后者多见于第 9 章 HM 风格类型方案（type scheme）
$\forall X.T$	$\exists X.T$	前者是全称类型，后者是存在类型
$S <: T$	$S = T$	前者是子类型关系，后者是相等
$\Gamma \vdash t : T$	$t \Downarrow v$	前者是类型判断，后者是求值关系
$\mu X.T$	无限展开的类型	前者是显式递归类型构造，后者通常是第 9 章 occur check 要阻止的隐式无限类型（infinite type）
$\text{fold}(t)$ / $\text{unfold}(t)$	直接类型相等	前者对应 iso-recursive 视角下的显式往返，后者不是“自动视为同一类型”

八、最后的阅读建议

如果你在阅读正文时总是被符号绊住，可以优先只抓住下面这几类最核心记号：

项的形状
- $\lambda x.t$
- $t_1\ t_2$
类型判断
- $\Gamma \vdash t : T$
计算关系
- $\longrightarrow$
- $\Downarrow$
多态与子类型
- $\forall X.T$
- $S <: T$
资源使用
- $\text{lin}$
- $\text{un}$

先把这些记号读顺，再回头看更细的符号，通常会轻松不少。

Keyboard shortcuts

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