编辑“︁Lean递归函数”︁

= Lean递归函数 =

'''Lean递归函数'''是Lean定理证明器中实现重复计算的核心构造，它允许函数通过调用自身来解决问题。递归在函数式编程和数学归纳证明中具有基础性地位，是处理归纳定义数据类型（如自然数、列表、树等）的必备工具。

== 基本概念 ==

在Lean中，递归函数必须满足'''终止性'''（Termination）条件，即所有递归调用必须作用于"更小"的参数，以确保计算最终会停止。这与数学归纳法的原理紧密相关。

递归函数的定义通常包含两个部分：
* '''基例'''（Base Case）：处理最简单的情况，无需递归
* '''递归情况'''（Recursive Case）：将问题分解为更小的子问题

=== 简单示例：阶乘函数 ===

以下是用Lean定义的阶乘函数：

<syntaxhighlight lang="lean">
def factorial : Nat → Nat
| 0     => 1  -- 基例：0! = 1
| n + 1 => (n + 1) * factorial n  -- 递归情况：(n+1)! = (n+1) * n!
</syntaxhighlight>

'''输入输出示例'''：
* `#eval factorial 5` → 120
* `#eval factorial 0` → 1

== 结构递归与良基递归 ==

Lean主要支持两种安全的递归形式：

=== 1. 结构递归 ===
递归调用只作用于参数的直接子结构，这是最简单的形式：

<syntaxhighlight lang="lean">
def list_length {α : Type} : List α → Nat
| []      => 0
| _ :: xs => 1 + list_length xs
</syntaxhighlight>

=== 2. 良基递归 ===
当结构递归不适用时，可以使用'''well-founded recursion'''，它依赖一个显式的终止证明：

<syntaxhighlight lang="lean">
def ackermann : Nat → Nat → Nat
| 0,   n   => n + 1
| m+1, 0   => ackermann m 1
| m+1, n+1 => ackermann m (ackermann (m + 1) n)
termination_by ackermann m n => (m, n)
</syntaxhighlight>

== 递归原理图 ==

<mermaid>
graph TD
    A[递归函数调用] -->|参数更小| B[递归调用]
    B --> C[继续分解]
    C -->|达到基例| D[返回结果]
    D --> E[组合结果]
</mermaid>

== 递归与归纳的关系 ==

在Lean中，递归和归纳是紧密相关的概念。递归函数的正确性通常需要用归纳法来证明。例如，证明`factorial`函数的正确性：

<math>
\text{factorial}(n) = \prod_{k=1}^n k
</math>

== 实际应用案例 ==

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

<syntaxhighlight lang="lean">
inductive BinaryTree (α : Type) where
| leaf : BinaryTree α
| node : BinaryTree α → α → BinaryTree α → BinaryTree α

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

=== 案例2：快速排序 ===

<syntaxhighlight lang="lean">
def quicksort : List Int → List Int
| [] => []
| x :: xs =>
    let smaller := quicksort (xs.filter (· ≤ x))
    let larger := quicksort (xs.filter (· > x))
    smaller ++ [x] ++ larger
</syntaxhighlight>

== 常见问题与调试 ==

1. '''非终止递归'''错误：
   - 确保每次递归调用参数都在减小
   - 使用`termination_by`子句显式指定终止度量

2. '''效率问题'''：
   - 避免重复计算（可考虑记忆化）
   - 尾递归优化（Lean会自动优化部分情况）

== 高级主题 ==

=== 互递归 ===
多个函数相互调用：

<syntaxhighlight lang="lean">
mutual
def even : Nat → Bool
| 0 => true
| n + 1 => odd n

def odd : Nat → Bool
| 0 => false
| n + 1 => even n
end
</syntaxhighlight>

=== 递归定理证明 ===
递归不仅用于计算，也用于证明：

<syntaxhighlight lang="lean">
theorem factorial_pos : ∀ n, 0 < factorial n
| 0     => by simp [factorial]
| n + 1 => by
    rw [factorial]
    exact Nat.mul_pos (Nat.succ_pos n) (factorial_pos n)
</syntaxhighlight>

== 总结 ==

Lean中的递归函数是强大的工具，它：
* 遵循数学归纳原理
* 需要保证终止性
* 可用于计算和证明
* 支持多种递归模式

掌握递归是理解Lean和函数式编程的关键步骤。初学者应从结构递归开始，逐步学习更复杂的递归形式。

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