归纳递归

归纳递归是对归纳类型 (或归纳族) 的扩展, 允许构造子的类型一定程度地违反严格正性, 极大地提高了类型论的证明论强度.

也可以对高阶归纳类型进行类似的拓展, 得到 “高阶归纳递归”.

也可以对互归纳进行类似的拓展, 得到 “互归纳递归”. 再加上互递归对互归纳的特殊情况, 可以得到 “互归纳互递归”. 将这些功能全部放到一起, 可以合成出 “高阶互归纳互递归” 的类型, 这是在依值类型论中定义自己的有力工具.

1定义

定义 1.1. 在语境 $Γ$ 中, 一组归纳递归的定义是二元组 $(D, f)$ :

•	$Γ ⊢ D : A \to U$ 是一个像归纳族的类型,

•	$Γ ⊢ f : D \to X$ 是一个简单类型的函数 ( $X$ 是任意类型, 可以引用语境 $Γ$ , 但不能引用参数), 在这个阶段姑且当作公理,

•	$D$ 的构造子 $Γ ⊢ con_{i} : \prod_{x : C_{i}} D (u_{i})$ 的参数 $C_{i}$ 由满足严格正性的类型或者对 $f$ 的函数应用 (这里超出了归纳类型的能力, 但该类型仍然很像一个归纳类型) 生成,

•	有了构造子后, 推出 $D$ 对应的消去子,

•	$f$ 使用 $D$ 的消去子定义出函数的行为.

使用互递归消除的手法可以将归纳递归拓展到一个类型、多个函数的情况. 若需要考虑多个类型, 则需要用到互归纳.

若要非常严格地形式化定义而不用到公理、切换定义的属性等 “违规” 操作, 则需要用到语汇理论.

例 3.1. 依值类型论的 Tarski 宇宙可以使用归纳递归在类型论内部定义. 此处给出一个仅含 $Π$ 类型的定义:

•	$U : U$ 是宇宙——它的实例对应类型的表示,
•	$el : U \to U$ 对于每个类型的表示, 给出对应的类型,
•	$π : \prod_{A : U} \prod_{B : el (A) \to E} U$ 是 $Π$ 类型的表示, 其中 $A$ 是定义域的类型的表示、 $B$ 是值域的类型的表示, 很明显, $B$ 是一个含有 $A$ 的实例的表达式,
•	$el (π (A, B)) = \prod_{x : el (A)} el (B (x))$ 使用模式匹配的语法定义了 $el$ .

该例子演示了归纳递归提高证明论强度的原因: 它可以将类型论自己的宇宙表示出来.

•	Peter Dybjer (2003). “A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory”. Journal of Symbolic Logic 65. (doi)

术语翻译

归纳递归 • 英文 induction-recursion