λ演算中的有类型赋值系统 我们先从λ演算的基础开始。λ演算是一种形式系统，用于描述函数定义、函数应用和递归。在无类型λ演算中，项可以任意应用，但这会导致一些项无法归一化（即计算不终止）。有类型λ演算通过引入类型来约束项的形成规则，从而确保所有项都有良定的计算行为。 接下来，我们讨论简单类型λ演算（→-演算）。这里只有一种类型构造子：函数类型→。类型通常由语法τ ::= α | τ → τ给出，其中α是基本类型。项和类型的关联通过类型赋值规则实现，例如：(Var) 如果x:τ在上下文Γ中，则Γ ⊢ x:τ；(Abs) 如果Γ, x:σ ⊢ M:τ，则Γ ⊢ (λx.M):σ→τ；(App) 如果Γ ⊢ M:σ→τ且Γ ⊢ N:σ，则Γ ⊢ (M N):τ。这个系统具有强归一化性：每个良类型项都会在有限步内归约到范式。 现在，我们考虑多态类型系统，例如系统F（或二阶λ演算）。它引入了类型变量和全称量化，允许项具有“对于所有类型”的多态行为。类型形式为τ ::= α | τ → τ | ∀α.τ。关键规则是：(TypeAbs) 如果Γ ⊢ M:τ且α不在Γ中自由出现，则Γ ⊢ (Λα.M):∀α.τ；(TypeApp) 如果Γ ⊢ M:∀α.τ，则Γ ⊢ (M σ):τ[ σ/α ]。这大大提高了表达力，但类型推断变得不可判定。 最后，我们探讨依赖类型系统，如λΠ-演算（LF）。在这里，类型可以依赖于项，模糊了类型和项之间的界限。类型本身有种类（kind），形成层次：种类Kind ::= Type | (x:τ)Kind。规则包括：(Pi) 如果Γ ⊢ A:Type且Γ, x:A ⊢ B:Type，则Γ ⊢ (Πx:A.B):Type；(Lam) 如果Γ, x:A ⊢ M:B，则Γ ⊢ (λx.M):(Πx:A.B)。这允许表达非常丰富的规范，用于定理证明和高级程序验证。