•2025年09月
type-theory

Implementing Path Induction for Identity Types in Dependent Systems

在依赖类型系统中，通过J消除器实现路径归纳，用于处理身份类型的等式证明，提供不依赖单值公理的工程化参数和证明模式。

在依赖类型理论中，身份类型（Identity Types）是处理等式证明的核心机制。它将等式视为类型，从而将证明转化为类型的居民（inhabitants）。路径归纳（Path Induction）作为身份类型的消除规则，允许我们通过指定自反路径（reflexive paths）的行为来定义对任意路径的函数。这在不引入单值公理（Univalence Axiom）的情况下，就能高效处理等式证明，尤其适用于形式化验证和类型安全的编程系统如Agda或Coq。

路径归纳的核心在于J消除器（J Eliminator），它体现了类型理论的计算原则：只需为自反路径refl(a)提供行为，就能唯一地扩展到所有路径。这种机制避免了穷举所有可能证明的复杂性，转而利用路径的结构进行归纳推理。相比传统数学中的等式关系，路径归纳将等式证明视为连续的“路径”，这在同伦类型论（Homotopy Type Theory, HoTT）中进一步扩展，但即使在马丁-洛夫类型理论（Martin-Löf Type Theory, MLTT）的标准框架下，也足以支持许多实用证明。

考虑身份类型的定义。在依赖类型系统中，身份类型Id_A(x, y)表示类型A中从x到y的路径类型。其引入规则是refl(a) : Id_A(a, a)，即自反路径。对于任意x, y : A和p : Id_A(x, y)，J允许定义一个依赖函数J(x, y, p) : D(x, y, p)，其中D是依赖于端点x, y和路径p的类型族。只需提供d(a) : D(a, a, refl(a))，J就会确保J(a, a, refl(a)) ≡ d(a)，从而计算性地扩展到非自反路径。

这一规则的证据源于类型理论的归纳原则。身份类型类似于归纳类型，其唯一构造器refl决定了消除规则的形式。这类似于对自然数的归纳：只需指定零和后继的行为，就能定义对所有自然数的函数。路径归纳的计算行为确保了在refl上的定义直接影响整个路径空间，避免了非构造性假设。在HoTT中，这对应于路径的“填充”性质，但无需单值公理，我们仍能证明路径的基本代数，如连接（concatenation）和逆（inverse）。

在实际实现中，以Agda为例，我们可以直接定义身份类型和J消除器。Agda的标准库中，_≡_类型即为身份类型：

data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x

infix 20 ≡

J的定义如下：

J : {A : Set} (D : (x y : A) → x ≡ y → Set) → ((a : A) → D a a refl) → (x y : A) (p : x ≡ y) → D x y p J D d x .x refl = d x

此定义体现了J的通用性：D可以是任意依赖类型族，d指定了refl的情况。计算规则J D d a a refl ≡ d a确保了类型居民的唯一性。

一个典型应用是路径连接_∙_，定义为从x到z的路径，通过y中间点：

∙ : {A : Set} {x y z : A} (p : x ≡ y) (q : y ≡ z) → x ≡ z p ∙ q = J (λ x y p → (z : A) → (q' : y ≡ z) → x ≡ z) (λ _ z q' → q') x y p z q

这里，D(x, y, p) = Π(z : A)(q' : y ≡ z) x ≡ z，d(a) z q' = q'。当p = refl时，x ≡ z简化为y ≡ z，即q'，这符合直观。类似地，路径逆_⁻¹使用J证明y ≡ x，通过D(x, y, p) = y ≡ x，d(a) = refl。

这些操作的证明依赖路径归纳的模式：对α : p ≡ q，使用J归纳于α，动机为refl上的平凡情况。无需单值，我们能证明连接的单位律，如iₗ : p ≡ refl ∙ p，通过J于D(x, y, p) = p ≡ refl ∙ p，d(a) = refl。

在工程实践中，实现路径归纳需注意参数选择：

  1. 定义D的依赖性：D应尽可能弱，以简化d。参数化端点x, y确保泛化；若D仅依赖p，则退化为函数扩展。

  2. 动机d的构造：d(a)必须计算性地匹配refl行为。使用refl作为基例，避免循环定义。清单：(i) 验证d(a) : D(a, a, refl(a))；(ii) 确保无额外假设；(iii) 测试计算J ... refl ≡ d(a)。

  3. 阈值与监控：在证明中，路径长度（维度）作为阈值；高维路径需多重J嵌套。监控点：计算规则是否折叠refl；若不，检查D的依赖。回滚策略：若J失败，退至模式匹配（pattern matching），但牺牲计算性。

  4. 清单 for 证明：

    • 步骤1：形式化目标为D(x, y, p)。
    • 步骤2：构造d(a)，证明其类型。
    • 步骤3：应用J，验证计算行为。
    • 步骤4：泛化至任意路径，使用连接/逆组合。

例如，证明连接的右单位iᵣ : p ≡ p ∙ refl，使用J于D(x, y, p) = p ≡ p ∙ refl，d(a) = refl。证据：J计算于refl给出refl，扩展至p。

路径归纳的局限在于标准MLTT中路径非单值：等价不即等式。但通过J模式，我们能处理大多数代数证明，如群同构，而无需额外公理。在编译器或效果系统中，这可用于等式重写规则的验证，确保类型安全而不引入不一致。

总之，路径归纳提供了一种高效、计算性的等式证明框架。通过J消除器，我们在依赖类型系统中实现身份类型的全功能，支持形式化开发。实际参数如D的弱化和d的计算性，确保可落地性；在HoTT应用中，它桥接了类型与几何，直至单值扩展。（字数：1024）