Lean递归类型

Lean递归类型是Lean定理证明器类型系统中用于定义自引用数据结构的重要工具。它允许类型构造器在其定义中引用自身，从而能够表示如自然数、列表、树等无限或递归结构。本文将系统介绍递归类型的核心概念、语法形式、归纳原则及实际应用。

基本概念

递归类型（Recursive Type）是指其定义中包含对自身引用的类型。在Lean中，这类类型通过`inductive`关键字定义，并遵循严格的正性检查（positivity）规则以确保逻辑一致性。

递归类型的关键特征包括：

• 自引用：类型定义中直接或间接引用自身
• 基础情形：至少包含一个不依赖自引用的构造子（终止条件）
• 递归情形：包含至少一个依赖自引用的构造子

数学上可表示为：若类型$T$的定义中包含形如$T \rightarrow ... \rightarrow T$的构造子，则$T$是递归类型。

语法结构

Lean中定义递归类型的基本语法如下：

inductive TypeName where
  | constructor₁ : ArgumentType₁ → ... → TypeName
  | constructor₂ : ArgumentType₂ → ... → TypeName
  ...
  | constructorₙ : ArgumentTypeₙ → ... → TypeName

经典示例：自然数

自然数的Peano定义是递归类型的典型示例：

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

此定义包含：

• 基础情形：`zero`表示0
• 递归情形：`succ`接收一个Nat返回其后继

递归原理

Lean会为每个递归类型自动生成： 1. 递归子（recursor）：用于模式匹配和递归定义 2. 归纳原则：用于数学归纳法证明

例如对于`Nat`，Lean自动生成：

Nat.rec : {motive : Nat → Sort u} →
  motive Nat.zero →
  ((n : Nat) → motive n → motive (Nat.succ n)) →
  (t : Nat) → motive t

实际案例

案例1：二叉树

定义二叉树结构：

inductive BinaryTree (α : Type) where
  | leaf : BinaryTree α
  | node (left : BinaryTree α) (val : α) (right : BinaryTree α) : BinaryTree α

graph TD A[node] --> B[left subtree] A --> C[value] A --> D[right subtree] B --> E[leaf] D --> F[leaf]

案例2：列表类型

Lean标准库中`List`的核心定义：

inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

计算列表长度的递归函数：

def length {α : Type} : List α → Nat
  | List.nil => 0
  | List.cons _ tail => 1 + length tail

#eval length (List.cons 1 (List.cons 2 List.nil))  -- 输出: 2

互递归类型

Lean支持相互递归的类型定义，需使用`mutual`关键字：

mutual
  inductive Even where
    | zero : Even
    | succOdd (n : Odd) : Even

  inductive Odd where
    | succEven (n : Even) : Odd
end

正性检查

Lean会进行正性检查（positivity condition）确保递归定义不会导致逻辑矛盾。以下非法定义将被拒绝：

-- 非法的负递归
inductive IllegalType where
  | c : (IllegalType → Bool) → IllegalType  -- 错误！

高级主题：归纳递归类型

结合归纳和递归的更复杂类型，如可表示无限树的W类型：

inductive W (α : Type u) (β : α → Type v) where
  | mk (a : α) (f : β a → W α β) : W α β

常见问题

问题	解决方案
递归不终止	确保所有递归路径最终到达基础情形
无法推导类型	显式添加类型注解
正性检查失败	重构类型定义避免负位置出现

总结

递归类型是Lean类型系统的核心组成部分，它们：

• 提供表达递归数据结构的能力
• 自动生成相关归纳原则
• 支持复杂的数学对象建模
• 通过严格检查保证逻辑一致性

掌握递归类型对于理解Lean中的数据类型定义和定理证明至关重要。