编辑“︁Lean归纳类型”︁

{{DISPLAYTITLE:Lean归纳类型}}

'''Lean归纳类型'''（Inductive Types）是[[Lean定理证明器]]类型系统的核心概念之一，它允许用户通过有限的规则构造复杂的数据结构和逻辑命题。本文将详细介绍归纳类型的定义、语法、应用场景以及与递归类型的关系。

== 基本概念 ==

归纳类型是通过一组'''构造子'''（constructors）定义的类型，每个构造子可以包含参数并递归引用类型自身。数学上，归纳类型 <math>T</math> 的构造过程可描述为：

<math>
T = c_1(\tau_{11}, \ldots, \tau_{1n_1}) \mid \cdots \mid c_k(\tau_{k1}, \ldots, \tau_{kn_k})
</math>

其中 <math>c_i</math> 是构造子，<math>\tau_{ij}</math> 是其参数类型。

=== 关键特性 ===
* 构造子是唯一的生成方式
* 支持模式匹配（pattern matching）
* 允许递归定义（如自然数、链表）

== 语法与示例 ==

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

这个经典定义表示：
* <code>zero</code> 是 0 的构造子
* <code>succ</code> 接收一个 <code>Nat</code> 返回其后继

=== 模式匹配 ===
定义加法函数：
<syntaxhighlight lang="lean">
def add : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.succ (add n m)

#eval add (Nat.succ Nat.zero) (Nat.succ (Nat.succ Nat.zero))  -- 输出: 3
</syntaxhighlight>

== 递归与归纳 ==

归纳类型天然支持结构归纳法。例如证明加法交换律：
<syntaxhighlight lang="lean">
theorem add_comm (n m : Nat) : add n m = add m n := by
  induction m with
  | zero => simp [add]
  | succ m ih => rw [add, ih, ← Nat.succ_add]
</syntaxhighlight>

== 复杂类型示例 ==

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

=== 二叉树 ===
<mermaid>
graph TD
    A[Tree α] --> B[leaf]
    A --> C[node]
    C --> D[left: Tree α]
    C --> E[val: α]
    C --> F[right: Tree α]
</mermaid>

对应定义：
<syntaxhighlight lang="lean">
inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Tree α → α → Tree α → Tree α
</syntaxhighlight>

== 实际应用 ==

=== 表达式求值 ===
定义算术表达式：
<syntaxhighlight lang="lean">
inductive Expr where
  | const : Int → Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr

def eval : Expr → Int
  | Expr.const n => n
  | Expr.add a b => eval a + eval b
  | Expr.mul a b => eval a * eval b
</syntaxhighlight>

=== 逻辑命题 ===
构造命题逻辑：
<syntaxhighlight lang="lean">
inductive PropForm where
  | true : PropForm
  | false : PropForm
  | var : String → PropForm
  | and : PropForm → PropForm → PropForm
  | or : PropForm → PropForm → PropForm
</syntaxhighlight>

== 高级主题 ==

=== 互归纳类型 ===
多个相互依赖的类型：
<syntaxhighlight lang="lean">
mutual
  inductive Even where
    | zero : Even
    | succOdd : Odd → Even

  inductive Odd where
    | succEven : Even → Odd
end
</syntaxhighlight>

=== 索引归纳类型 ===
使用参数化构造：
<syntaxhighlight lang="lean">
inductive Vec (α : Type) : Nat → Type where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)
</syntaxhighlight>

== 参见 ==
* [[依赖类型]]
* [[递归类型]]
* [[构造演算]]

{{类型系统导航}}

[[Category:Lean编程]]
[[Category:类型理论]]

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