λ演算中的有类型λ演算 有类型λ演算通过为λ项赋予类型来扩展无类型λ演算，其核心目标是避免逻辑悖论（如罗素悖论）和确保计算的可预测性。下面分步骤说明其核心概念与规则： 类型的基本定义 类型是描述项行为的形式化标签。例如，自然数类型（如 Nat ）或函数类型（如 Nat → Bool ）。 类型通过语法规则递归定义： 基类型 ：如 Nat 、 Bool 等原子类型。 函数类型 ：若 A 和 B 是类型，则 A → B 表示输入为 A 类型、输出为 B 类型的函数。 项与类型的关联规则 每个项需通过类型标注明确其类型，例如 λx:A. M 表示输入 x 具有类型 A ， M 为函数体。 类型判断 ：形式为 Γ ⊢ M : A ，表示在类型上下文 Γ （一组变量的类型假设）下，项 M 具有类型 A 。 类型推导的推理规则 变量规则 ：若变量 x 的类型在上下文中定义，则直接推导： \[ \frac{x:A ∈ Γ}{Γ ⊢ x:A} \] 函数应用规则 ：若 M 是函数类型 A → B ， N 是类型 A ，则应用结果类型为 B ： \[ \frac{Γ ⊢ M : A → B \quad Γ ⊢ N : A}{Γ ⊢ M N : B} \] 函数抽象规则 ：若在扩展上下文 Γ, x:A 下 M 的类型为 B ，则抽象后的函数类型为 A → B ： \[ \frac{Γ, x:A ⊢ M : B}{Γ ⊢ (λx:A. M) : A → B} \] 类型系统的意义与性质 安全性 ：类型系统保证“类型良好的项不会卡住”——即不会出现非预期的计算错误（如将整数作为函数调用）。 规范化定理 ：在简单类型λ演算中，所有良类型项均强规范化，即计算必在有限步内终止。 表达力限制 ：简单类型无法支持递归（如阶乘函数），需通过扩展类型（如递归类型或系统 F）恢复图灵完备性。 常见类型系统扩展 多态类型 ：允许类型参数化（如 ∀α. α → α ），提升代码复用性。 依赖类型 ：允许类型依赖项的值（如 Vec A n 表示长度为 n 的列表），用于形式化验证。 通过类型约束，有类型λ演算在程序语言设计（如 ML、Haskell）和定理证明（如 Coq）中成为形式化推理的基石。