编辑“︁Lean递归类型”︁

{{DISPLAYTITLE:Lean递归类型}}

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

== 基本概念 ==

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

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

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

== 语法结构 ==

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

<syntaxhighlight lang="lean">
inductive TypeName where
  | constructor₁ : ArgumentType₁ → ... → TypeName
  | constructor₂ : ArgumentType₂ → ... → TypeName
  ...
  | constructorₙ : ArgumentTypeₙ → ... → TypeName
</syntaxhighlight>

=== 经典示例：自然数 ===

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

<syntaxhighlight lang="lean">
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat
</syntaxhighlight>

此定义包含：
* 基础情形：`zero`表示0
* 递归情形：`succ`接收一个Nat返回其后继

== 递归原理 ==

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

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

<syntaxhighlight lang="lean">
Nat.rec : {motive : Nat → Sort u} →
  motive Nat.zero →
  ((n : Nat) → motive n → motive (Nat.succ n)) →
  (t : Nat) → motive t
</syntaxhighlight>

== 实际案例 ==

=== 案例1：二叉树 ===

定义二叉树结构：

<syntaxhighlight lang="lean">
inductive BinaryTree (α : Type) where
  | leaf : BinaryTree α
  | node (left : BinaryTree α) (val : α) (right : BinaryTree α) : BinaryTree α
</syntaxhighlight>

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

=== 案例2：列表类型 ===

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

<syntaxhighlight lang="lean">
inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 互递归类型 ==

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

<syntaxhighlight lang="lean">
mutual
  inductive Even where
    | zero : Even
    | succOdd (n : Odd) : Even

  inductive Odd where
    | succEven (n : Even) : Odd
end
</syntaxhighlight>

== 正性检查 ==

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

<syntaxhighlight lang="lean">
-- 非法的负递归
inductive IllegalType where
  | c : (IllegalType → Bool) → IllegalType  -- 错误！
</syntaxhighlight>

== 高级主题：归纳递归类型 ==

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

<syntaxhighlight lang="lean">
inductive W (α : Type u) (β : α → Type v) where
  | mk (a : α) (f : β a → W α β) : W α β
</syntaxhighlight>

== 常见问题 ==

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

== 总结 ==

递归类型是Lean类型系统的核心组成部分，它们：
* 提供表达递归数据结构的能力
* 自动生成相关归纳原则
* 支持复杂的数学对象建模
* 通过严格检查保证逻辑一致性

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean类型系统]]