编辑“︁Lean递归函数”︁

= Lean递归函数 =

'''Lean递归函数'''是Lean函数式编程中的核心概念之一，它允许函数通过调用自身来解决复杂问题。递归在数学和计算机科学中广泛应用，尤其在处理递归数据结构（如列表、树等）时尤为高效。本节将详细介绍Lean中的递归函数，包括其基本语法、终止性保证、模式匹配以及实际应用案例。

== 递归函数的基本概念 ==

递归函数是指在函数定义中调用自身的函数。在Lean中，递归函数必须满足'''终止性'''（Termination），即函数调用最终会停止，否则会导致无限循环。Lean的类型系统会检查递归函数的终止性，确保程序的正确性。

递归通常用于解决可以分解为更小子问题的问题，例如计算阶乘、斐波那契数列或遍历树结构。

=== 递归函数的语法 ===

在Lean中，递归函数使用`def`关键字定义，并通过`:=`指定函数体。递归调用必须满足结构递归（Structural Recursion）或提供明确的终止证明。

<syntaxhighlight lang="lean">
-- 计算阶乘的递归函数
def factorial : Nat → Nat
  | 0 => 1  -- 基本情况
  | (n + 1) => (n + 1) * factorial n  -- 递归情况
</syntaxhighlight>

'''输入示例：'''
<syntaxhighlight lang="lean">
#eval factorial 5  -- 输出: 120
</syntaxhighlight>

'''解释：'''
* 当输入为`0`时，函数返回`1`（基本情况）。
* 当输入为`n + 1`时，函数递归计算`factorial n`，并将结果乘以`n + 1`（递归情况）。

== 结构递归与终止性 ==

Lean要求递归函数必须是'''结构递归'''的，即递归调用必须作用于原始参数的严格子结构。例如，在列表递归中，递归调用必须作用于列表的尾部。

<syntaxhighlight lang="lean">
-- 计算列表长度的递归函数
def length {α : Type} : List α → Nat
  | [] => 0  -- 空列表长度为0
  | _ :: xs => 1 + length xs  -- 非空列表长度为1加上尾部长度
</syntaxhighlight>

'''输入示例：'''
<syntaxhighlight lang="lean">
#eval length [1, 2, 3]  -- 输出: 3
</syntaxhighlight>

'''解释：'''
* 空列表`[]`的长度为`0`。
* 非空列表`_ :: xs`的长度为`1`加上`xs`的长度（递归调用）。

=== 终止性证明 ===

如果递归不是结构递归，Lean会要求提供终止性证明。例如，以下函数使用`termination_by`指定终止条件：

<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>

'''输入示例：'''
<syntaxhighlight lang="lean">
#eval ackermann 2 1  -- 输出: 5
</syntaxhighlight>

'''解释：'''
* `termination_by`指定了终止条件，确保递归调用最终停止。

== 递归与模式匹配 ==

Lean支持通过模式匹配（Pattern Matching）简化递归函数的定义。模式匹配可以同时处理多种输入情况，使代码更清晰。

<syntaxhighlight lang="lean">
-- 使用模式匹配的递归函数（计算斐波那契数列）
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | (n + 2) => fib (n + 1) + fib n
</syntaxhighlight>

'''输入示例：'''
<syntaxhighlight lang="lean">
#eval fib 6  -- 输出: 8
</syntaxhighlight>

'''解释：'''
* `fib 0`返回`0`，`fib 1`返回`1`。
* 对于`n + 2`，递归计算`fib (n + 1)`和`fib n`，并求和。

== 递归的实际应用 ==

递归在函数式编程中广泛应用，以下是一些实际案例：

=== 1. 列表反转 ===
<syntaxhighlight lang="lean">
def reverse {α : Type} : List α → List α
  | [] => []
  | x :: xs => reverse xs ++ [x]
</syntaxhighlight>

'''输入示例：'''
<syntaxhighlight lang="lean">
#eval reverse [1, 2, 3]  -- 输出: [3, 2, 1]
</syntaxhighlight>

=== 2. 二叉树遍历 ===
<syntaxhighlight lang="lean">
inductive Tree (α : Type) where
  | empty : Tree α
  | node (left : Tree α) (val : α) (right : Tree α) : Tree α

def size {α : Type} : Tree α → Nat
  | Tree.empty => 0
  | Tree.node l _ r => 1 + size l + size r
</syntaxhighlight>

'''输入示例：'''
<syntaxhighlight lang="lean">
def sampleTree := Tree.node (Tree.node Tree.empty 1 Tree.empty) 2 (Tree.node Tree.empty 3 Tree.empty)
#eval size sampleTree  -- 输出: 3
</syntaxhighlight>

=== 3. 快速排序 ===
<syntaxhighlight lang="lean">
def qsort : List Nat → List Nat
  | [] => []
  | x :: xs =>
    let smaller := qsort (xs.filter (· ≤ x))
    let larger := qsort (xs.filter (· > x))
    smaller ++ [x] ++ larger
</syntaxhighlight>

'''输入示例：'''
<syntaxhighlight lang="lean">
#eval qsort [5, 2, 9, 1, 3]  -- 输出: [1, 2, 3, 5, 9]
</syntaxhighlight>

== 递归的可视化 ==

递归调用可以通过调用栈可视化。以下是一个阶乘函数的调用流程：

<mermaid>
graph TD
  A["factorial(3)"] --> B["3 * factorial(2)"]
  B --> C["2 * factorial(1)"]
  C --> D["1 * factorial(0)"]
  D --> E["1"]
  E --> C["2 * 1 = 2"]
  C --> B["3 * 2 = 6"]
  B --> A["返回6"]
</mermaid>

== 数学公式支持 ==

递归函数的正确性可以通过数学归纳法证明。例如，阶乘函数的性质可以表示为：
<math>
n! = \begin{cases}
1 & \text{如果 } n = 0, \\
n \times (n-1)! & \text{如果 } n > 0.
\end{cases}
</math>

== 总结 ==

* Lean递归函数通过调用自身解决问题，必须满足终止性。
* 结构递归是Lean中的常见模式，确保函数终止。
* 模式匹配简化递归函数的定义。
* 递归广泛应用于列表处理、树遍历和排序算法。

通过本节的学习，读者应能掌握Lean递归函数的基本原理和实践方法，并能够编写高效的递归程序。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean函数式编程]]