Lean递归函数[编辑 | 编辑源代码]

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

基本概念[编辑 | 编辑源代码]

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

递归函数的定义通常包含两个部分：

基例（Base Case）：处理最简单的情况，无需递归
递归情况（Recursive Case）：将问题分解为更小的子问题

简单示例：阶乘函数[编辑 | 编辑源代码]

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

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

输入输出示例：

`#eval factorial 5` → 120
`#eval factorial 0` → 1

结构递归与良基递归[编辑 | 编辑源代码]

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

1. 结构递归[编辑 | 编辑源代码]

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

def list_length {α : Type} : List α → Nat
| []      => 0
| _ :: xs => 1 + list_length xs

2. 良基递归[编辑 | 编辑源代码]

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

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)

递归原理图[编辑 | 编辑源代码]

递归与归纳的关系[编辑 | 编辑源代码]

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

$factorial (n) = \prod_{k = 1}^{n} k$

实际应用案例[编辑 | 编辑源代码]

案例1：二叉树遍历[编辑 | 编辑源代码]

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)

案例2：快速排序[编辑 | 编辑源代码]

def quicksort : List Int → List Int
| [] => []
| x :: xs =>
    let smaller := quicksort (xs.filter (· ≤ x))
    let larger := quicksort (xs.filter (· > x))
    smaller ++ [x] ++ larger

常见问题与调试[编辑 | 编辑源代码]

1. 非终止递归错误：

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

2. 效率问题：

  - 避免重复计算（可考虑记忆化）
  - 尾递归优化（Lean会自动优化部分情况）

高级主题[编辑 | 编辑源代码]

互递归[编辑 | 编辑源代码]

多个函数相互调用：

mutual
def even : Nat → Bool
| 0 => true
| n + 1 => odd n

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

递归定理证明[编辑 | 编辑源代码]

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

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)

总结[编辑 | 编辑源代码]

Lean中的递归函数是强大的工具，它：

遵循数学归纳原理
需要保证终止性
可用于计算和证明
支持多种递归模式

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