λ演算中的有类型λ-演算 从无类型到有类型的动机 在无类型λ演算中，项可以自由组合（如 (λx.xx)(λx.xx) ），这导致非终止计算和逻辑悖论。有类型λ演算通过为项赋予 类型 ，限制组合规则，排除无意义项（如自应用 xx 若 x 非函数类型），同时确保计算的 规范性 （如强正规化性质）。 类型语法与判断规则 定义简单类型λ演算（Simply Typed λ-Calculus, STLC）： 类型语法 ： τ ::= base | τ → τ （基础类型如 nat ，函数类型如 nat → bool ）。 项语法 ： t ::= x | λx:τ.t | t t （变量、抽象、应用）。 类型判断 ：使用上下文 Γ （类型假设集合）和判断 Γ ⊢ t : τ ，通过推理规则赋值： 变量规则 ： Γ, x:τ ⊢ x : τ 抽象规则 ：若 Γ, x:τ₁ ⊢ t : τ₂ ，则 Γ ⊢ (λx:τ₁.t) : τ₁ → τ₂ 应用规则 ：若 Γ ⊢ t₁ : τ₁ → τ₂ 且 Γ ⊢ t₂ : τ₁ ，则 Γ ⊢ t₁ t₂ : τ₂ 类型安全与元理论 STLC 满足两大核心性质： 进展性 ：良类型项要么是值（如抽象项 λx.t ），要么可继续规约。 保持性 ：若 Γ ⊢ t : τ 且 t → t‘ ，则 Γ ⊢ t’ : τ 。 这构成类型安全的基础，并隐含 强正规化定理 ：所有良类型项均终止。 类型系统扩展与计算表达力 为增强表达力，引入多态、递归等扩展： 系统F （多态λ演算）：通过全称类型 ∀α.τ 支持参数多态，可编码自然数、链表等数据结构。 依赖类型 ：允许类型依赖项（如 Vec n 表示长度为 n 的向量），在类型层面编码复杂约束。 递归类型 ：通过 μα.τ 表达自引用结构（如列表 μα.Unit + (nat × α) ），结合不动点组合子实现通用递归。 与逻辑和计算的深层联系 有类型λ演算通过 Curry-Howard 同构 关联逻辑系统： STLC 对应直觉主义命题逻辑（ → 为逻辑蕴含）。 系统F 对应二阶命题逻辑，依赖类型对应一阶谓词逻辑。 这一桥梁使类型论成为证明辅助工具（如 Coq、Agda）的基础，实现“程序即证明”。