编辑“︁Lean归纳类型”︁（章节）

= Lean归纳类型 =

'''Lean归纳类型'''（Inductive Types）是Lean定理证明器中最基础且强大的类型构造方式之一，它允许用户通过归纳的方式定义数据类型和命题。归纳类型在函数式编程和形式化验证中广泛应用，是理解依赖类型理论和证明构造的核心概念。

== 简介 ==

归纳类型是通过一组构造子（constructors）递归定义的类型。每个构造子可以接受零个或多个参数，并返回该归纳类型的实例。在Lean中，归纳类型不仅用于表示数据结构（如列表、树），还能表示逻辑命题（如“真”、“假”或“存在”）。

归纳类型的定义遵循以下形式：
<syntaxhighlight lang="lean">
inductive MyType where
  | constructor₁ : Arg₁ → ... → Argₙ → MyType
  | constructor₂ : ... → MyType
  ...
</syntaxhighlight>

=== 基本示例：自然数 ===
自然数的归纳定义是经典的例子：
<syntaxhighlight lang="lean">
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat
</syntaxhighlight>
这里：
* <code>zero</code> 是自然数0的构造子。
* <code>succ</code> 接受一个<code>Nat</code>类型的参数<code>n</code>，返回<code>n + 1</code>。

=== 递归与模式匹配 ===
归纳类型通常与递归函数和模式匹配结合使用。例如，计算自然数的加法：
<syntaxhighlight lang="lean">
def add : Nat → Nat → Nat
  | m, Nat.zero   => m
  | m, Nat.succ n => Nat.succ (add m n)
</syntaxhighlight>
输入 <code>add 2 3</code> 会逐步展开为 <code>Nat.succ (Nat.succ (Nat.succ 2))</code>，最终输出 <code>5</code>。

== 归纳类型的分类 ==
归纳类型可分为以下几类：
1. '''简单归纳类型'''：如<code>Nat</code>、<code>Bool</code>。
2. '''参数化归纳类型'''：如<code>List α</code>（泛型列表）。
3. '''索引归纳类型'''：构造子的返回类型依赖参数（如长度索引列表）。
4. '''互归纳类型'''：多个相互依赖的归纳类型。

=== 参数化示例：列表 ===
<syntaxhighlight lang="lean">
inductive List (α : Type) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α
</syntaxhighlight>
* <code>nil</code> 表示空列表。
* <code>cons</code> 将元素<code>head</code>添加到列表<code>tail</code>前。

== 实际应用案例 ==
=== 二叉树的定义与操作 ===
定义二叉树并实现其深度计算：
<syntaxhighlight lang="lean">
inductive BinaryTree (α : Type) where
  | leaf : BinaryTree α
  | node (left : BinaryTree α) (val : α) (right : BinaryTree α) : BinaryTree α

def depth : BinaryTree α → Nat
  | BinaryTree.leaf => 0
  | BinaryTree.node l _ r => 1 + max (depth l) (depth r)
</syntaxhighlight>

=== 命题逻辑的编码 ===
归纳类型可编码逻辑命题。例如，定义命题的合取与析取：
<syntaxhighlight lang="lean">
inductive PropForm where
  | true  : PropForm
  | false : PropForm
  | and   : PropForm → PropForm → PropForm
  | or    : PropForm → PropForm → PropForm
</syntaxhighlight>

== 高级主题：归纳类型的原理 ==
Lean中归纳类型的底层实现基于'''归纳族'''（Inductive Families）和'''递归-归纳原则'''。例如，<code>Nat</code>会自动生成归纳原则：
<math>
\forall P : \mathbb{N} \to \text{Prop}, P(0) \to (\forall n, P(n) \to P(n+1)) \to \forall n, P(n)
</math>

== 图表展示 ==
<mermaid>
graph TD
  A[归纳类型] --> B[简单类型]
  A --> C[参数化类型]
  A --> D[索引类型]
  A --> E[互归纳类型]
  B --> F[Nat, Bool]
  C --> G[List α]
  D --> H[Vec n α]
  E --> I[Even/Odd]
</mermaid>

== 常见问题 ==
* '''Q: 归纳类型和递归类型的区别？'''  
  A: 归纳类型强调通过构造子定义，递归类型强调自引用（如链表）。在Lean中二者通常统一。
* '''Q: 如何避免非终止递归？'''  
  A: Lean会检查递归函数是否结构递归（即参数在每次调用中严格减小）。

== 总结 ==
归纳类型是Lean中定义数据结构和逻辑的基础工具，支持从简单自然数到复杂命题的编码。通过构造子和模式匹配，用户可以构建类型安全的程序和形式化证明。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean归纳与递归]]