在依赖类型理论中，身份类型（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。
在工程实践中，实现路径归纳需注意参数选择：
-
定义 D 的依赖性：D 应尽可能弱，以简化 d。参数化端点 x, y 确保泛化；若 D 仅依赖 p，则退化为函数扩展。
-
动机 d 的构造：d (a) 必须计算性地匹配 refl 行为。使用 refl 作为基例，避免循环定义。清单：(i) 验证 d (a) : D (a, a, refl (a))；(ii) 确保无额外假设；(iii) 测试计算 J ... refl ≡ d (a)。
-
阈值与监控：在证明中，路径长度（维度）作为阈值；高维路径需多重 J 嵌套。监控点：计算规则是否折叠 refl；若不，检查 D 的依赖。回滚策略：若 J 失败，退至模式匹配（pattern matching），但牺牲计算性。
-
清单 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）