λ演算中的有类型λ-演算 有类型λ-演算通过为项赋予类型来扩展无类型λ-演算，从而在语法层面排除某些不合理的项（如自应用），同时保持计算的表达能力。下面我将逐步介绍其核心概念。 类型的基本构成 类型由基础类型（如 Nat 、 Bool ）和函数类型（如 A → B ）通过语法规则递归定义。例如，若 A 和 B 是类型，则 A → B 表示输入类型为 A 、输出类型为 B 的函数类型。 类型系统的目标是确保每个项都有唯一确定的类型，并通过类型规则在项构造过程中验证类型一致性。 类型上下文与判断 类型上下文（记为 Γ ）是一个有限映射，将变量与类型关联（如 x:A, y:B ）。它记录了当前作用域内变量的类型信息。 类型判断的形式为 Γ ⊢ M : A ，表示在上下文 Γ 下，项 M 具有类型 A 。例如，若 Γ 包含 x:A ，则 Γ ⊢ x : A 成立。 类型规则 变量规则 ：若变量 x 的类型在上下文中定义为 A ，则可以直接推断其类型： Γ, x:A ⊢ x : A 。 函数抽象规则 ：若在扩展上下文 Γ, x:A 下，项 M 的类型为 B ，则可构造函数 λx.M ，其类型为 A → B 。规则写为： Γ, x:A ⊢ M : B ⇒ Γ ⊢ (λx.M) : A → B 。 函数应用规则 ：若项 M 的类型为 A → B ，项 N 的类型为 A ，则应用 M N 的类型为 B 。规则为： Γ ⊢ M : A → B 且 Γ ⊢ N : A ⇒ Γ ⊢ (M N) : B 。 类型安全性与规约 类型系统保证“良类型项不会卡住”：若 Γ ⊢ M : A 且 M 可规约，则规约后的项仍具有类型 A （保持引理），且要么是值，要么可继续规约（进展引理）。 例如，项 (λx:Nat. x) 5 中，若 5 被赋予类型 Nat ，应用规则确保规约结果 5 的类型仍为 Nat 。 类型系统的扩展与变体 简单类型λ-演算可扩展为多态类型（如System F），允许类型变量和通用量化，从而支持更灵活的多态函数。 依赖类型系统（如LF）进一步允许类型依赖项，使得类型可表达更复杂的规范（如列表长度）。