本术语表用于统一本教程中的中英文术语和最小定义。它的目标不是替代正文，而是帮助你在阅读时快速确认：
- 这个词在本教程里具体指什么；
- 它和相近概念有什么区别；
- 它在英文文献中通常对应哪个词；
- 它主要在哪一章进入主线讨论。
阅读提示
- 术语表中的定义以“本教程语境下够用”为原则，力求简明。
- 某些术语在不同文献中会有更强或更弱的版本；若存在这种情况，条目中会尽量提示。
- 术语表中的公式只用于帮助识别，不替代正文中的完整规则与推导。
- 为了把本附录同时做成“术语索引”，各小节标题后都补上了“主要对应章节”；若你忘了某个概念最该回看哪里，可以先看这些导航。
- 若正文中某个术语首次出现时给了英文原文，而你后来又忘了，也可以直接回到这里统一查。
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 项 | term | 形式系统中的语法对象。在 Lambda 演算中，项由变量、抽象、应用等构造生成。 | 第 2–3 章 |
| 变量 | variable | 出现在项中的名字，如 x、y、z。 | 第 2–3 章 |
| 抽象 | abstraction | 函数定义，记作 λx.t。其中 x 是参数，t 是函数体。 | 第 3 章 |
| 应用 | application | 函数调用，记作 t1 t2，表示把 t1 应用于 t2。 | 第 3 章 |
| 绑定变量 | bound variable | 被某个抽象绑定的变量出现。例如在 λx.t 中，由这个 λx 管辖的 x 是绑定的。 | 第 3 章 |
| 自由变量 | free variable | 不受任何抽象绑定的变量出现。自由变量反映一个项对外部环境的依赖。 | 第 3 章 |
| 自由变量集合 | set of free variables | 记作 FV(t)，表示项 t 中所有自由变量的集合。 | 第 3 章 |
| 作用域 | scope | 某个绑定生效的语法范围。 | 第 3 章 |
| 封闭项 | closed term | 没有自由变量的项。 | 第 3 章 |
| 组合子 | combinator | 在很多语境下，指没有自由变量的 Lambda 项。为避免歧义，本教程更常使用“封闭项”；在讨论 S、K、I 时会保留“组合子”这一说法。 | 第 3 章、附录E |
| α-等价 | alpha-equivalence | 只改变绑定变量名字而不改变绑定结构时得到的等价关系。 | 第 3 章 |
| α-重命名 / α-转换 | alpha-renaming / alpha-conversion | 安全地修改绑定变量名，以避免冲突或变量捕获。 | 第 3 章 |
| 替换 | substitution | 记作 [x ↦ s]t，表示把 t 中自由出现的 x 替换为 s。 | 第 3 章 |
| 避免捕获的替换 | capture-avoiding substitution | 替换时保证不会把原本自由的变量意外变成绑定变量。 | 第 3–4 章 |
| 变量捕获 | variable capture | 替换过程中，自由变量因同名绑定而被错误“吃掉”的现象。 | 第 3 章 |
| 新鲜变量 | fresh variable | 一个当前上下文中尚未使用、因此不会引发冲突的变量名。 | 第 3 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| β-归约 | beta-reduction | Lambda 演算的核心计算规则：(λx.t) s → [x ↦ s]t。 | 第 4 章 |
| β-redex / 可归约表达式 | beta-redex / reducible expression | 形如 (λx.t) s 的项，可执行一次 β-归约。文献中常简称 redex。 | 第 4 章 |
| 归约关系 | reduction relation | 描述一个项如何一步变成另一个项的关系。 | 第 4 章 |
| 单步归约 | one-step reduction | 记作 t → t'，表示 t 经过一步计算变成 t'。 | 第 4 章 |
| 多步归约 | multi-step reduction | 记作 t →* t'，表示经过零步或多步计算从 t 到达 t'。 | 第 4 章 |
| 范式 | normal form | 相对于某个归约关系，已经无法继续归约的项。 | 第 4 章 |
| 值 | value | 相对于某个求值策略，被视为“计算完成”的项形态。值与范式相关，但不是同一个概念。 | 第 4 章、第 5 章 |
| 发散 | divergence | 一个项永远继续归约、无法到达范式的现象。 | 第 4 章、附录D |
| 合流性 | confluence | 若一个项能沿不同路径归约，则这些路径仍可重新汇合的性质。 | 第 4 章 |
| Church–Rosser 定理 | Church–Rosser theorem | Lambda 演算合流性的经典结果。其重要推论是：若某项有范式，则该范式在 α-等价意义下唯一。 | 第 4 章 |
| 归约策略 | reduction strategy | 当一个项中有多个可归约位置时，优先选择哪一个归约。 | 第 4 章 |
| 求值策略 | evaluation strategy | 编程语言层面对“先算哪里、何时把参数算成值”的更具体约定。 | 第 4 章、附录D、附录E |
| 传名调用 | call-by-name | 调用函数时，不先把参数求值为值，而是先把参数项代入函数体。 | 第 4 章、附录D |
| 传值调用 | call-by-value | 调用函数时，先把参数求值为值，再进行函数应用。 | 第 4 章、附录D、附录E |
| 按需求值 | call-by-need | 一种与传名调用接近但带共享的惰性求值策略。Haskell 通常以此为典型例子。 | 第 4 章 |
| 小步语义 | small-step semantics | 通过单步关系 t → t' 描述程序如何一步步执行。 | 第 4–5 章 |
| 大步语义 | big-step semantics | 通过关系 t ⇓ v 直接描述程序最终求值到什么结果。 | 第 4 章 |
| 卡住状态 | stuck term / stuck state | 既不是值，又无法继续按照求值规则前进的项。这个概念通常在扩展语言（如带布尔值、自然数等）中讨论最自然。 | 第 4–5 章 |
| η-归约 | eta-reduction | 形如 λx. f x → f 的化简，通常要求 x 不自由出现在 f 中。它表达了函数外延性的一种形式。 | 第 4 章（补充概念） |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 类型 | type | 对项进行静态分类的标签，用来约束其可能的计算行为。 | 第 5 章 |
| 类型系统 | type system | 一种可判定的语法方法，通过为程序片段赋予类型，排除某类被禁止的错误行为。 | 第 0 章、第 5 章 |
| 类型判断 | type judgment | 形如 Γ ⊢ t : T 的判断，表示“在环境 Γ 下，项 t 的类型是 T”。 | 第 5 章 |
| 类型环境 | type context / typing environment | 变量到类型的有限映射，通常记作 Γ。 | 第 5 章 |
| 类型规则 | typing rule | 规定什么条件下可以推出某个类型判断的推导规则。 | 第 5 章 |
| 类型检查 | type checking | 在给定必要类型信息的情况下，验证一个项是否符合类型规则。 | 第 5 章 |
| 类型推断 | type inference | 在类型注解不完整或缺失时，自动恢复类型信息。 | 第 9 章 |
| 良类型 | well-typed | 一个项若能在某环境下导出合法类型判断，则称其在该环境下良类型。 | 第 5 章 |
| 类型安全 | type safety / type soundness | 在选定语言与错误模型下，良类型程序不会进入被系统禁止的坏状态。常通过进展性与保持性表达。 | 第 5 章 |
| 进展性 | progress | 良类型的封闭项要么已经是值，要么还可以继续求值。 | 第 5 章 |
| 保持性 | preservation | 若 Γ ⊢ t : T 且 t → t'，则仍有 Γ ⊢ t' : T。也常称 subject reduction。 | 第 5 章 |
| subject reduction | subject reduction | 保持性的常见别名，强调“归约保持类型”。 | 第 5 章 |
| 可判定性 | decidability | 存在一个总会在有限时间内结束的过程，用来判断某个性质是否成立。 | 第 0 章、第 5 章 |
| 声明式类型规则 | declarative typing | 先说明“什么情况下一个类型判断成立”的规则写法，不一定直接对应最简洁的检查算法。 | 第 5–6 章 |
| 语法制导 | syntax-directed | 规则与语法构造直接对应，因此检查过程通常可以沿语法树递归进行。 | 第 5–6 章 |
| 代换引理 | substitution lemma | 若某项在扩展环境下良类型，而替换进去的值类型匹配，则替换后的项仍保持原类型。 | 第 5 章 |
| 强正规化 | strong normalization | 所有良类型项都在有限步内归约到范式的性质。不是所有类型系统都满足这一性质。 | 第 5 章、附录D |
| Church 风格 | Church-style | 项本身携带显式类型注解的风格，如 λx:T.t。 | 第 5 章 |
| Curry 风格 | Curry-style | 项本身不直接携带类型注解，类型由外部规则或推断系统赋予的风格。 | 第 5 章、第 9 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 基础类型 | base type | 不再通过更小类型构造出来的类型，如 Bool、Nat、Unit。 | 第 6 章 |
| 单位类型 | unit type | 只有一个值的类型，常记作 Unit。它更接近“无有趣返回值的结果类型”，不应简单等同于 null。 | 第 6 章 |
| 自然数类型 | natural number type | 理想化的自然数类型，通常记作 Nat。它与现实语言中的机器整数相关，但不完全等同。 | 第 6 章 |
| 积类型 | product type | 形如 T1 × T2 的类型，表示同时包含一个 T1 和一个 T2。 | 第 6 章 |
| 和类型 | sum type | 形如 T1 + T2 的类型，表示“要么是 T1，要么是 T2”，通常带有标记。 | 第 6 章 |
| 左注入 | left injection | 构造和类型左侧分支的项，常写作 inl(t)。 | 第 6 章 |
| 右注入 | right injection | 构造和类型右侧分支的项，常写作 inr(t)。 | 第 6 章 |
| 分支分析 | case analysis | 对和类型值进行分类处理的形式，通常写作 case ... of ...。 | 第 6 章 |
| 记录类型 | record type | 带字段名的积类型，如 {name:String, age:Nat}。在本教程后续子类型讨论中，默认按结构性记录来理解。 | 第 6 章、第 8 章 |
| 递归类型 | recursive type | 允许类型引用自身的类型，常写作 μX.T。 | 第 6 章 |
| 同构递归 | iso-recursive | 把 μX.T 与其展开式看作非常接近、但仍需显式 fold / unfold 往返的递归类型视角。 | 第 6 章 |
| 等价递归 | equi-recursive | 把 μX.T 与其展开式直接视为同一个类型的递归类型视角。 | 第 6 章 |
| fold | fold | 把递归类型展开后的结构重新“包回”递归类型。 | 第 6 章 |
| unfold | unfold | 把递归类型“打开一层”，得到其展开形式。 | 第 6 章 |
| 可变引用 | mutable reference | 指向某个可变存储位置的引用类型，常写作 Ref(T)。 | 第 6 章、第 8 章 |
| 解引用 | dereference | 从引用中读出其当前内容的操作。 | 第 6 章 |
| 赋值 | assignment | 向某个可变引用写入新值的操作。 | 第 6 章 |
| 存储类型 | store typing | 在带可变存储的语言中，用来跟踪堆中位置应存储何种类型信息的辅助结构。 | 第 6 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 参数化多态 | parametric polymorphism | 程序对任意类型都以统一方式工作的一类多态。 | 第 7 章 |
| 二阶类型系统 | second-order type system | 允许对类型变量进行抽象与应用的类型系统。 | 第 7 章 |
| System F | System F | 最经典的参数化多态理论系统之一，也叫二阶 Lambda 演算。 | 第 7 章 |
| 类型变量 | type variable | 出现在类型中的占位符，如 X、Y、α。 | 第 7 章、第 9 章 |
| 全称类型 | universal type | 形如 ∀X.T 的类型，表示“对任意类型 X，都有 T”。 | 第 7 章、第 9 章 |
| 类型抽象 | type abstraction | 对类型变量的抽象，常写作 ΛX.t。 | 第 7 章 |
| 类型应用 | type application | 把多态项实例化到某个具体类型，常写作 t[T]。 | 第 7 章 |
| 存在类型 | existential type | 形如 ∃X.T 的类型，表示存在某个类型 X 使 T 成立，常用于隐藏实现类型。 | 第 7 章 |
| 打包 | pack | 把某个具体实现连同其隐藏类型一起封装成存在类型值。 | 第 7 章 |
| 拆包 | unpack | 打开存在类型值，在受限作用域内以抽象方式使用其隐藏实现。 | 第 7 章 |
| 抽象数据类型 | abstract data type (ADT) | 隐藏内部表示，只暴露操作接口的数据抽象方式。注意这里的 ADT 指 abstract data type，不是 algebraic data type。 | 第 7 章 |
| 类型算子 | type operator | 以类型为输入、产生新类型的类型层函数。 | 第 7 章 |
| kind / 种类 | kind | 用来区分“普通类型”“从类型到类型的构造器”等层级的分类工具。本教程只做方向性介绍。 | 第 7 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 子类型 | subtype | 若 S <: T，表示任何需要 T 的地方都可以安全地使用 S。 | 第 8 章 |
| 安全替换 | safe substitution / safe replacement | 子类型最核心的直觉：更具体的值可以放到要求更一般类型的位置。 | 第 8 章 |
| subsumption | subsumption | 通过 S <: T 把一个已有类型 S 的项提升为类型 T 的规则。 | 第 8 章 |
| 自反性 | reflexivity | 子类型关系满足 T <: T。 | 第 8 章 |
| 传递性 | transitivity | 若 S <: U 且 U <: T，则 S <: T。 | 第 8 章 |
| 宽度子类型化 | width subtyping | 对记录而言，字段更多的记录可作为字段更少记录的子类型。 | 第 8 章 |
| 深度子类型化 | depth subtyping | 对记录而言，若对应字段类型更具体，则整体记录类型也可更具体。 | 第 8 章 |
| 协变 | covariance | 子类型关系与类型构造方向一致。常见于函数返回值、许多只读结构。 | 第 8 章 |
| 逆变 | contravariance | 子类型关系与类型构造方向相反。经典例子是函数参数。 | 第 8 章 |
| 不变 | invariance | 既不协变也不逆变，通常要求类型完全相同。可变引用常是这种情形。 | 第 8 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| Hindley–Milner | Hindley–Milner (HM) | 最经典的可推断多态类型系统之一。本章主要以它为背景介绍类型推断。 | 第 9 章 |
| 约束生成 | constraint generation | 从项结构出发，收集“这些类型必须相等 / 必须匹配”的条件。 | 第 9 章 |
| 合一 | unification | 求解类型等式，寻找使这些等式同时成立的替换。 | 第 9 章 |
| 替换 | substitution | 把类型变量统一替换成具体类型或其他类型表达式的映射。 | 第 9 章 |
| 最一般合一器 | most general unifier (MGU) | 在所有能解决约束的替换中，最不“多做承诺”的那个。 | 第 9 章 |
| occur check | occur check | 在合一时检查一个类型变量是否出现在待替换目标内部，以防构造无限类型。 | 第 9 章 |
| 无限类型 | infinite type | 形如 α = α -> β 这类需要无限展开的类型。标准 HM 不允许。 | 第 9 章 |
| 类型方案 | type scheme | 可被多次实例化的一类类型，通常写作 ∀α1...αn.T。在 HM 中，它主要出现在环境里，而不是像 System F 那样直接作为对象语言项的一部分。 | 第 9 章 |
| 主类型 | principal type | 在给定系统中，一个项最一般、最不多做承诺的类型；若其他可赋予的类型都可由它实例化得到，就称它是主类型。 | 第 9 章 |
| 主类型方案 | principal type scheme | 对多态绑定而言，最一般的类型方案；HM 系统的重要性质之一就是很多项都存在主类型方案。 | 第 9 章 |
| 泛化 | generalization | 在 let 绑定处，把不受当前环境约束的类型变量量化为类型方案。 | 第 9 章 |
| 实例化 | instantiation | 在使用多态绑定时，把类型方案中的量化变量替换为新的具体类型或新鲜类型变量。 | 第 9 章 |
| let 多态 | let polymorphism | let 绑定的名字可以被泛化为多态类型方案，并在不同使用点独立实例化。 | 第 9 章 |
| 算法 W | Algorithm W | HM 推断的经典算法。它递归推断项的类型，并返回替换与类型。 | 第 9 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 子结构类型系统 | substructural type system | 通过禁止部分结构规则来限制变量使用方式的类型系统。 | 第 10 章 |
| 结构规则 | structural rules | 逻辑与类型环境中关于假设使用方式的规则，如交换、弱化、收缩。 | 第 10 章 |
| 交换 | exchange | 允许改变环境中假设的顺序。 | 第 10 章 |
| 弱化 | weakening | 允许把一个根本没用到的假设加入环境。 | 第 10 章 |
| 收缩 | contraction | 允许同一假设被重复使用。 | 第 10 章 |
| 线性类型 | linear type | 要求变量恰好使用一次的类型纪律。 | 第 10 章 |
| 仿射类型 | affine type | 要求变量至多使用一次。与线性相比，允许不用。 | 第 10 章 |
| 相关类型 | relevant type | 要求变量至少使用一次。 | 第 10 章 |
| 有序类型 | ordered type | 要求变量恰好使用一次，并且按环境顺序使用。 | 第 10 章 |
| 限定符 | qualifier | 用来区分线性值与无限制值的标记，如 lin 与 un。 | 第 10 章 |
| 环境分裂 | context splitting | 在应用等需要两个子推导的地方，把环境划分给左右子项的机制；线性变量通常只能分给一侧。 | 第 10 章 |
| 线性函数 | linear function | 在参数使用上服从线性纪律的函数类型，常记作 A ⊸ B 或类似变体。 | 第 10 章 |
| 无限制值 | unrestricted value | 可以自由复制、丢弃和重排使用的普通值。 | 第 10 章 |
| 所有权 | ownership | 资源由哪个绑定负责使用与释放的纪律。Rust 中常以此实现仿射式资源控制。 | 第 10 章 |
| 借用 | borrowing | 在不转移所有权的情况下临时获得访问权限的机制。 | 第 10 章 |
| 会话类型 | session type | 用于描述通信协议的类型系统，常与线性 / 有序资源思想相关。 | 第 10 章 |
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 推导规则 | inference rule | 形如“若前提成立则结论成立”的形式化规则。 | 第 1 章、第 5 章 |
| 推导树 | derivation tree | 由推导规则逐层构造出的树形证明对象。 | 第 1 章、第 5 章 |
| 公理 | axiom | 没有前提的推导规则。 | 第 1 章 |
| 归纳定义 | inductive definition | 通过基础情况与构造规则定义一个无限对象族的方法。 | 第 1–3 章 |
| 结构归纳法 | structural induction | 对按归纳定义生成的对象结构做归纳证明的方法。 | 第 1 章、第 5 章 |
| 推导归纳法 | induction on derivations | 对推导树结构做归纳的证明方法。 | 第 1 章、第 5 章 |
| Curry–Howard 对应 | Curry–Howard correspondence | 在合适的形式系统中，“类型对应命题、项对应证明”的深刻联系。 | 第 6–7 章 |
| 合取 | conjunction | 逻辑中的“且”，常与积类型对应。 | 第 6 章 |
| 析取 | disjunction | 逻辑中的“或”，常与和类型对应。 | 第 6 章 |
| 蕴含 | implication | 逻辑中的“如果……那么……”，常与函数类型对应。 | 第 5 章 |
- 值是相对于求值策略定义的“计算完成形式”；
- 范式是相对于某个归约关系定义的“无法继续归约”；
- 在简单系统里二者常重合，但来源不同，不应直接混为一谈。
- 封闭项的定义是“没有自由变量的项”；
- 组合子在很多文献里常指封闭 Lambda 项，尤其在
S、K、I 语境中；
- 为避免歧义，本教程优先使用“封闭项”，并在适合时说明其与“组合子”的关系。
- abstract data type：强调隐藏表示、暴露接口；
- algebraic data type：通常指由和类型、积类型等代数组合得到的数据类型；
- 两者英文缩写都常写成 ADT，因此阅读时必须看上下文，不应直接混用。
- 类型检查：给定足够多的类型信息，验证程序是否符合规则；
- 类型推断：在类型信息缺失时，自动恢复这些信息；
- 二者相关，但不是一回事。
- Church 风格：项中显式写类型注解；
- Curry 风格：项中不直接写类型注解，类型由系统外部赋予或推断；
- “显式 / 隐式”只是表面差异，背后关系到检查与推断方式。
下面这些词主要出现在进阶附录中，但为了让本附录更像全书索引，这里也统一收录。
| 中文 | 英文 | 本教程中的含义 | 主要回看 |
|---|
| 不动点 | fixed point | 若 f(x) = x，则称 x 是 f 的一个不动点。 | 附录D |
| 不动点组合子 | fixed-point combinator | 给定函数 f，能够构造出某种不动点的 Lambda 项。 | 附录D |
| Y 组合子 | Y combinator | 最经典的不动点组合子之一，通常与传名调用语境联系最紧。 | 附录D |
| Z 组合子 | Z combinator | 为传值调用语境常见的递归编码而使用的一个变体不动点组合子。 | 附录D |
| Church 编码 | Church encoding | 用函数来表示布尔值、自然数等数据与操作的一类编码方法。 | 附录E |
| Church 布尔值 | Church booleans | 把布尔值编码成“二选一函数”的表示方式。 | 附录E |
| Church 数 | Church numerals | 把自然数编码成“重复作用若干次”的高阶函数。 | 附录E |
如果把本教程中的术语主线压缩成一句话，可以这样说：
语法定义程序长什么样，语义定义程序如何计算，类型系统定义哪些程序被允许，而元理论说明这些限制为什么可靠。
术语表中的大多数词，最终都可以放回这条主线中理解；而“主要回看”这一列，则是帮助你把这些术语重新挂回对应章节的导航索引。