编辑“︁Lean良基归纳”︁

{{DISPLAYTITLE:Lean良基归纳}}

'''良基归纳'''（Well-founded Recursion）是Lean定理证明器中一种基于[[良基关系]]的归纳方法，它允许在满足特定终止条件的前提下进行递归定义和归纳证明。本文将从基础概念到实际应用全面介绍Lean中的良基归纳。

== 基本概念 ==

良基归纳的核心思想是：在一个集合上定义的递归函数或归纳证明，必须基于某种'''良基关系'''（Well-founded relation），这种关系确保递归调用总是在“更小”的元素上进行，从而保证终止性。

数学上，集合<math>A</math>上的二元关系<math><</math>是良基的，当且仅当不存在无限递减链：
<math>a_0 > a_1 > a_2 > \cdots</math>

在Lean中，良基归纳通过`WellFounded`类型类实现，典型应用包括：
* 非结构递归（如基于整数大小的递归）
* 复杂数据结构的归纳（如树或图的遍历）
* 无法直接使用结构归纳的情况

== 语法与实现 ==

Lean中使用`wellFounded_induction`进行良基归纳。基本模式如下：

<syntaxhighlight lang="lean">
theorem example (x : α) : P x :=
  wellFounded_induction wf (λ y IH, ...)
where
  `wf`是良基关系证明
  `IH`是归纳假设（对所有`y < x`有`P y`）
</syntaxhighlight>

=== 基础示例：整数递减 ===

定义一个基于整数绝对值的良基递归函数：

<syntaxhighlight lang="lean">
def factorial : ℤ → ℕ
| n :=
  if h : n ≤ 0 then 1
  else n * factorial (n - 1)
termination_by _ => n  -- 指定度量标准
decreasing_by simp [h] -- 证明递归参数减小
</syntaxhighlight>

'''输入/输出示例'''：
<pre>
#eval factorial 5  -- 输出: 120
#eval factorial (-3) -- 输出: 1（根据基线条件）
</pre>

== 良基关系构造 ==

在Lean中构造良基关系的常见方法：

=== 1. 使用预定义关系 ===
Lean标准库提供了许多良基关系，如：
* `<` 在自然数上
* `⊂` 在有限集合上

=== 2. 子关系构造 ===
若<math>r \subseteq s</math>且<math>s</math>良基，则<math>r</math>也良基。

=== 3. 逆像构造 ===
给定函数<math>f : α → β</math>和<math>β</math>上的良基关系<math><_β</math>，可定义<math>α</math>上的关系：
<math>a <_α a' := f a <_β f a'</math>

== 高级案例：阿克曼函数 ==

阿克曼函数是经典的良基递归案例：

<syntaxhighlight lang="lean">
def ackermann : ℕ → ℕ → ℕ
| 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["ack(2,1)"] --> B["ack(1, ack(2,0))"]
    B --> C["ack(2,0) = ack(1,1)"]
    C --> D["ack(1,1) = ack(0, ack(1,0))"]
    D --> E["ack(1,0) = ack(0,1)"]
    E --> F["ack(0,1) = 2"]
    D --> G["ack(0,2) = 3"]
    C --> H["ack(1,2) = ack(0, ack(1,1))"]
    H --> G
    H --> I["ack(0,3) = 4"]
    B --> J["ack(1,3) = ack(0, ack(1,2))"]
    J --> I
    J --> K["ack(0,4) = 5"]
</mermaid>

== 实际应用场景 ==

=== 场景1：算法终止证明 ===
在证明合并排序的正确性时，需要证明：
<math>length (left l) < length l ∧ length (right l) < length l</math>
其中`left`和`right`是分割函数。

=== 场景2：游戏状态分析 ===
在棋类游戏中，可用良基归纳证明：
* 游戏状态转换关系是无环的
* 特定策略必然导致终止

== 常见问题与解决 ==

{| class="wikitable"
! 问题 !! 解决方案
|-
| 无法自动推断终止性 || 显式提供`termination_by`和`decreasing_by`
|-
| 递归参数复杂 || 使用词典序或组合度量
|-
| 需要自定义良基关系 || 构造逆像关系或子关系
|}

== 延伸阅读 ==

* Lean标准库中的`WellFounded`模块
* 数学基础中的[[序数]]理论
* 计算理论中的[[停机问题]]关联

[[Category:Lean编程]]
[[Category:定理证明]]
[[Category:递归理论]]

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