消去子、递归子与归纳原理

形式陈述 ​

归纳类型公理库归纳类型Inductive type · Inductive datatype由有限构造步骤生成的最小递归数据类型，并以严格正性保障其递归结构良好。的构造器规定如何产生值，消去子则规定如何完整地使用这些值。它们首先是声明式类型规则公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。，不等于某种模式匹配编译算法。对自然数，固定结果类型 $C$ 的非依赖递归子可写为

$${\mathsf{rec}}_{\mathbb{N}}:C\to (\mathbb{N}\to C\to C)\to \mathbb{N}\to C.$$

第一个参数处理 zero，第二个参数同时接收前驱 $n$ 与递归结果。其计算规则是

$$\begin{array}{rl}{\mathsf{rec}}_{\mathbb{N}}{c}_0{c}_s\mathsf{zero}& ⟶c_0,\\ {\mathsf{rec}}_{\mathbb{N}}{c}_0{c}_s(\mathsf{succ}n)& ⟶c_{s}n({\mathsf{rec}}_{\mathbb{N}}{c}_0{c}_{s}n).\end{array}$$

这两条 β/计算规则说明递归子遇到某个构造器时如何约简，不能只给类型而省略。若目标随输入变化，就需要以 motive $P:\mathbb{N}\to \mathsf{Type}$ 为索引的依赖消去子：

$${\mathsf{ind}}_{\mathbb{N}}:P(\mathsf{zero})\to (\mathrm{\Pi }n:\mathbb{N}.P(n)\to P(\mathsf{succ}n))\to \mathrm{\Pi }n:\mathbb{N}.P(n).$$

它的两个计算分支分别使用基例证据与归纳步证据。由Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。看，motive 是待证性质，递归调用的结果变成归纳假设；因此依赖消去同时给出归纳原理。普通递归只产生固定 $C$ 型结果，二者不能仅因都按构造器分支就视为同一种类型。

列表的非依赖消去常写成 fold：

$${\mathsf{fold}}_{\mathsf{List}}:C\to (A\to C\to C)\to \mathsf{List}(A)\to C,$$

并满足 fold c f nil → c 与 fold c f (cons a xs) → f a (fold c f xs)。某些理论还加入 η 或唯一性原理，声称任何遵守这些构造分支的函数都等于相应 fold；该结论可能是判断相等、命题相等或只在语义中成立，必须由具体理论另行说明。

直觉 ​

构造器像数据的入口，消去子则是一份覆盖全部入口的出口协议。自然数只有 zero 与 succ 两种来源，所以消费自然数时只需说明这两种情况；递归子还把较小结构已经算出的结果交给当前分支。数据定义与使用规则由此成对出现，避免程序凭空假设不存在的第三种情况。

依赖消去比普通 fold 多出一个关键自由度：返回类型可以随被处理的值变化。于是结果不再只是整数、列表或布尔值，也可以是“关于当前这个 $n$ 的证明”。归纳法不是附加在数据外部的口诀，而是归纳类型消去规则的依赖版本。

例子与边界 ​

列表求和取 $C=\mathbb{Z}$、空表分支 $0$、非空分支 $\lambda ar.a+r$；列表长度取 $C=\mathbb{N}$、空表分支 zero、非空分支忽略元素并对递归结果取 succ。两个函数共享 fold 的控制骨架，却以不同代数解释构造器。

证明“每个自然数右加零仍等于自身”时，令 $P(n)$ 为 $n+0=n$。zero 分支给出 $0+0=0$；succ n 分支接收归纳假设 $n+0=n$，再由加法计算规则与等式同余推出 $\mathsf{succ}(n)+0=\mathsf{succ}(n)$。这里结果类型确实依赖 $n$，普通 ${\mathsf{rec}}_{\mathbb{N}}$ 的固定 $C$ 不能直接表达这项证明。

表面模式匹配通常会编译为消去子，但只有覆盖检查确认所有构造器都被处理、递归/终止检查确认递归调用良基后，这种翻译才保留归纳类型的总性。含遗漏分支、任意递归或复杂 guard 的语言级 match 不能无条件与核心消去子等同。

推论与应用 ​

消去子把数据声明系统地转化为程序与证明接口。编译器可将模式匹配 elaboration 为核心 recursor，证明助理则从归纳声明生成递归原则、归纳原则及相应计算规则；生成过程是算法化工作，产物必须满足本页的声明式类型与约简规律。

fold 还可由初始代数的唯一同态刻画，常称 catamorphism。这一语义视角解释了结构递归为何可组合，但不会自动决定具体类型理论采用哪种 η 规则，也不会让非良基递归获得终止保证。

参考资料

• Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984，inductive elimination and computation rules。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，inductive types and recursors。
• The Coq Reference Manual and The Agda Reference Manual，generated eliminators, pattern matching, and termination checking。