归纳类型

形式陈述 ​

归纳类型由一组构造器的引入规则生成，并取满足这些规则的最小闭合类型。若用类型算子表示，可把它写成 $\mu X.F(X)$：$F$ 描述展开一层的构造形状，$\mu$ 表示最小不动点。这里的“最小”意为类型中只有通过有限次构造器应用得到的对象；具体模型可以在集合、域或类型论内部给出，不能脱离所用语义范畴只把它定义成集合交集。

自然数的引入规则为

$$\frac{}{\mathrm{\Gamma }⊢\mathsf{zero}:\mathsf{Nat}}\frac{\mathrm{\Gamma }⊢n:\mathsf{Nat}}{\mathrm{\Gamma }⊢\mathsf{succ}(n):\mathsf{Nat}}.$$

参数化列表则有

$$\frac{}{\mathrm{\Gamma }⊢\mathsf{nil}:\mathsf{List}(A)}\frac{\mathrm{\Gamma }⊢a:A\mathrm{\Gamma }⊢xs:\mathsf{List}(A)}{\mathrm{\Gamma }⊢\mathsf{cons}(a,xs):\mathsf{List}(A)}.$$

这些是声明式类型规则公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。：它们规定什么可作为值的证据，不等同于编译器的内存布局或模式匹配算法。消去、递归与归纳原则由构造器的完备性导出，但其计算规则应另行陈述，不能仅凭“有构造器”省略。

为使定义保持良基，递归变量通常必须在 $F$ 中严格正出现。直观地说，通向 $X$ 的路径不能穿过函数参数位置；$1+A\times X$ 合法，而 $X\to \mathsf{Bool}$ 把 $X$ 放在负位置，不能直接作为普通严格正归纳定义。不同类型理论的正性检查细节会随索引、宇宙与高阶参数变化，但都服务于单调性、终止性或逻辑一致性等相应元理论目标。

直觉 ​

归纳类型不是任意一个“提到自身”的类型方程，而是一份有限的出生证明。自然数只有两种来源：zero 直接生成一个值，succ 从已经生成的自然数再生成一个值。于是每个居民都带着有限构造历史，可以沿最后一个构造步骤拆解，并把问题递归地交给更早生成的部分。

这也解释了最小性。方程 $X\cong 1+X$ 可能在不同语义中有包含额外无限对象的解；归纳解释只保留 zero、succ zero、succ (succ zero) 等有限层对象。最大不动点式的共归纳解释才用于无限流等可持续观察的对象。

例子与边界 ​

每个自然数都形如 ${\mathsf{succ}}^n(\mathsf{zero})$，且 $n$ 有限。定义加法时，可按第一个参数的构造历史递归：add zero m = m，add (succ n) m = succ (add n m)。递归调用面对的是构造器内部严格更小的 $n$，所以这一定义的终止依据来自归纳结构，而不是函数名称恰好再次出现。

无限流 1,1,1,… 没有有限的最终构造树，因而不是上述列表归纳类型的一个普通值；它需要惰性逐步生产，或使用共归纳类型及生产性条件。另一个失败边界是 $X=X\to \mathsf{Bool}$：递归变量落在箭头左侧，构造一个 $X$ 反而要求消费 $X$，破坏按构造层数建立的单调增长，不能套用自然数式的结构归纳。

一般递归类型公理库递归类型Recursive type通过类型方程把类型变量递归绑定到包含自身的类型。中的 fold/unfold 只在类型与其一层展开之间转换。它们本身不说明居民是否由有限构造器生成，也不自动提供归纳假设。反过来，归纳类型的构造器往往由实现编译成标签和字段，但其理论含义是引入规则及最小性，而不是某个固定的运行时编码。

推论与应用 ​

归纳类型为结构递归、覆盖检查和归纳证明提供共同骨架。代数数据类型公理库代数数据类型Algebraic data type · Algebraic datatype以有限构造子的和、每个构造子字段的积以及可选递归组合数据形状的类型。若采用严格正递归并取良基的最小解释，就得到常见的归纳数据；证明助理还可把构造器生成相应的递归子和依赖消去原则。

依赖类型公理库依赖类型Dependent type类型表达式可依赖项值的类型系统构造。进一步允许归纳族由索引区分精确形状，例如长度索引向量。此时构造器不仅生成值，还约束结果索引；核心思想仍是有限生成与正性，但消去时必须让目标命题随索引变化，不能退化成普通固定结果类型的 fold。

参考资料

• Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984，inductive definitions and elimination。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，inductive and coinductive types。
• Thierry Coquand and Christine Paulin, “Inductively Defined Types,” COLOG-88, 1990，strict positivity and inductive definitions。