λ演算中的有类型赋值系统

我将从基础概念开始，循序渐进地讲解有类型赋值系统的核心内容。

1. 类型赋值系统的基本概念
   类型赋值系统是简单类型λ演算的一种表示方式，它不直接给λ项附加类型标注，而是通过推导规则来推断项的类型。系统包含三个核心组成部分：类型环境（上下文）、类型判断和类型推导规则。类型环境Γ是从变量到类型的有穷映射，记作x₁:A₁,...,xₙ:Aₙ；类型判断的形式为Γ ⊢ M : A，表示在环境Γ下，项M具有类型A。

2. 类型赋值规则
   系统包含以下三条核心推导规则：

• 变量规则：如果(x:A) ∈ Γ，那么Γ ⊢ x : A
• 函数应用规则：如果Γ ⊢ M : A→B 且 Γ ⊢ N : A，那么Γ ⊢ (M N) : B
• 函数抽象规则：如果Γ, x:A ⊢ M : B，那么Γ ⊢ (λx.M) : A→B

3. 推导树的构造过程
   类型推导以树形结构呈现。例如，对项λf.λx.f x，推导从最内层开始：假设环境Γ包含f:A→B, x:A，由变量规则得Γ ⊢ f : A→B和Γ ⊢ x : A，应用函数应用规则得Γ ⊢ (f x) : B，接着两次应用函数抽象规则得到 ⊢ λf.λx.f x : (A→B)→A→B。

4. 类型保持性与进展定理
   在有类型赋值系统中，类型保持性定理保证：如果Γ ⊢ M : A且M →β N，那么Γ ⊢ N : A。进展定理则确保良类型的闭项不会卡住——它要么是值（抽象），要么可以继续规约。这两个性质共同构成了类型安全性的核心内容。

5. 类型推断算法
   类型推断的目标是为给定的无类型λ项和类型环境，寻找可能的类型赋值。算法W是经典的解决方案：它通过遍历项的结构，生成并解类型等式约束。算法依次处理变量、应用和抽象情形，在抽象情形中会引入新的类型变量，最终通过合一算法求解约束方程组。

6. 多态性的扩展
   简单类型系统的一个限制是缺乏多态性。为此发展的二阶λ演算引入了类型抽象和类型应用，允许项以类型作为参数。相应的类型判断形式变为Γ ⊢ M : σ，其中σ可以是∀α.σ形式的多态类型，类型规则扩展包含类型抽象规则和类型实例化规则。

7. 类型赋值与Curry-Howard对应
   在Curry-Howard视角下，类型赋值系统与直觉主义逻辑的自然演绎系统同构：类型对应逻辑公式，λ项对应证明，规约对应证明化简。具体地，函数类型A→B对应蕴含式A⊃B，类型环境对应假设集，良类型项的存在性对应相应公式的可证性。