一张总览图
集合 Set
集合是一堆对象的容器，例如 N = {0,1,2,...}。后面的关系、函数、谓词，都建立在集合之上。
关系 Relation
关系就是一堆元组。二元关系 R ⊆ S × T 可以理解为从左边对象到右边对象的箭头集合。
函数 Function
函数是“输出唯一”的关系。偏函数允许某些输入没有结果；全函数要求每个输入都有唯一结果。
从关系理解偏函数和全函数
交互图：看每个输入有几条箭头
判断口诀
一般关系：同一个输入可以没有结果、一个结果、多个结果。
偏函数：每个输入最多一个结果。也就是：要么没定义，要么唯一。
全函数：每个输入恰好一个结果。也就是：既不能没有，也不能多个。
R ⊆ S × T
偏函数：若 (s,t₁)∈R 且 (s,t₂)∈R，则 t₁=t₂
全函数：偏函数 + dom(R)=S
几个容易混淆的点
undefined
f(x) ↑ 表示 f 在 x 上无定义。比如 pred(0) 在自然数前驱函数里无定义。
fail
f(x)=fail 是一种明确返回的失败结果。失败是可观察的结果，可以被建模为 T ∪ {fail}。
divergence
发散表示算不完、不会返回。它和 fail 不一样：fail 是返回了失败，divergence 是没有返回。
保持性：把它理解成“不变式”
定义的白话版
如果 s R s′ 且 P(s)，总能推出 P(s′)，那么就说性质 P 被关系 R 保持。
∀s,s′. (s R s′ ∧ P(s)) ⇒ P(s′)
把 R 想成“一步执行”，把 P 想成“好性质”。保持性就是说：执行一步不会把好状态变坏。
数字例子
令 S = Z，x R y 表示 y = x + 1，P(x) 表示 x ≥ 0。
如果 x 非负，那么 x+1 仍然非负，所以 P 被“加一”关系保持。
如果 R 改成 y = x - 1，那么从 0 可以走到 -1，非负性被破坏，所以 P 不被保持。
放回 TAPL：关系、函数、类型安全
| 记号 | 它是什么关系 | 是否像函数 | 直觉 |
|---|---|---|---|
t → t′ | 小步语义，R ⊆ Tm × Tm | 通常是偏函数 | 同一个 term 通常最多只有一个下一步；value 或 stuck term 没有下一步。 |
t ⇓ v | 大步语义，R ⊆ Tm × Val | 通常是偏函数 | 如果能算出值，值通常唯一；若存在死循环，就不是全函数。 |
Γ ⊢ t : T | 类型关系，可看作 (Γ,t) ↦ T | 简单类型系统里通常是偏函数 | 类型唯一性说明同一个 term 在同一上下文下最多一个类型；ill-typed term 没有类型。 |
typeof(Γ,t) | 实现里的类型检查函数 | 常建模为全函数到 Ty ∪ {fail} | 对每个输入都停机并返回：要么类型 T，要么 fail。 |
Type Safety 的核心句式
Γ ⊢ t : Tt → t′Γ ⊢ t′ : TPreservation 定理：如果 Γ ⊢ t : T 且 t → t′，那么 Γ ⊢ t′ : T。
这正是 2.1.10 的定义在类型系统里的核心应用：well-typed 是 P，小步求值是 R。