λ演算中的有类型系统的类型等价与子类型算法 类型等价的基本概念 在简单类型λ演算中，类型等价是类型系统的核心关系。若两个类型τ和σ在结构上完全一致，则称它们等价（记作τ ≡ σ）。例如： 基础类型（如 Nat , Bool ）仅与自身等价。 函数类型 τ₁ → τ₂ 与 σ₁ → σ₂ 等价，当且仅当 τ₁ ≡ σ₁ 且 τ₂ ≡ σ₂ 。 此关系通过 结构归纳 定义，是后续子类型判断的基础。 声明式子类型规则 子类型关系（记作τ <: σ）描述类型的可替换性，通常包含以下规则： 自反性 ：∀τ, τ <: τ 传递性 ：若τ <: σ且σ <: ρ，则τ <: ρ 函数子类型协变/逆变 ： 若 τ₂ <: σ₂ 且 σ₁ <: τ₁ ，则 (τ₁ → τ₂) <: (σ₁ → σ₂) （注意参数类型的逆变性与返回类型的协变性） 算法化子类型判断 声明式规则可能因传递性导致无限推导，需设计 算法子类型 （记作τ ≤ σ）： 基础类型仅当相同时成立（如 Nat ≤ Nat ）。 函数类型递归检查： (τ₁ → τ₂) ≤ (σ₁ → σ₂) 当且仅当 σ₁ ≤ τ₁ 且 τ₂ ≤ σ₂ 显式传递性被消除，通过递归调用避免循环。 记录类型的宽度与深度子类型 扩展系统支持记录类型（如 {x: Nat, y: Bool} ）： 宽度子类型 ：允许子类型记录拥有更多字段（如 {x: Nat, y: Bool, z: Int} <: {x: Nat, y: Bool} ）。 深度子类型 ：递归应用于字段类型（如 {f: τ} <: {f: σ} 当 τ <: σ ）。 算法需合并二者：检查超类型所有字段在子类型中存在，且对应字段类型满足深度子类型。 类型等价与子类型的交互 实际系统中常将类型等价嵌入子类型： 若τ ≡ σ，则直接判定τ ≤ σ 通过 规范形式 消除语法差异（如重命名字段、调整嵌套顺序） 例如： {x: Nat, y: Bool} ≡ {y: Bool, x: Nat} ，需在判断前规范化记录字段顺序。 并类型与交类型的子类型 支持复合类型时： 并类型（ τ ∨ σ ）：若 τ ≤ ρ 且 σ ≤ ρ ，则 (τ ∨ σ) ≤ ρ 交类型（ τ ∧ σ ）：若 ρ ≤ τ 且 ρ ≤ σ ，则 ρ ≤ (τ ∧ σ) 算法需同时处理分布律（如 τ ∧ (σ ∨ ρ) ≡ (τ ∧ σ) ∨ (τ ∧ ρ) ），通过展开规范化形式实现。 算法实现与终止性 为确保终止： 记录已比较的类型对避免循环（如记忆化集合 Memo(τ, σ) ） 对递归类型需展开一层后比较（μ-展开） 时间复杂度与类型结构大小相关，多项式时间内可判定。