编辑“︁Lean Acc关系”︁

= Lean Acc关系 =

'''Acc关系'''（Accessible Relation）是Lean定理证明器中用于处理归纳和递归定义的核心概念之一。它提供了一种严格且形式化的方式，确保递归函数的终止性，从而避免无限循环或逻辑矛盾。本页面将详细介绍Acc关系的定义、性质、使用方法及其在Lean中的实际应用。

== 介绍 ==

在数学和计算机科学中，许多递归定义需要满足'''良基性'''（Well-foundedness）才能保证其合法性。Acc关系正是Lean中表示良基关系的一种方式。具体来说，给定一个二元关系`r : α → α → Prop`，若`x : α`满足`Acc r x`，则表示从`x`出发不存在无限下降链`x ≻ x₁ ≻ x₂ ≻ ...`（其中`≻`表示关系`r`）。

换句话说，`Acc r x`断言“`x`在关系`r`下是可访问的”，即所有从`x`开始的`r`-递减序列必然终止。这一性质是定义递归函数或进行归纳证明时的关键工具。

== 定义与性质 ==

在Lean中，`Acc`是一个归纳定义的谓词，其定义如下：

<syntaxhighlight lang="lean">
inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
  | intro (x : α) (h : ∀ y, r y x → Acc r y) : Acc r x
</syntaxhighlight>

解释：
* `Acc r x`的构造器`intro`表明，若对于所有满足`r y x`的`y`，`Acc r y`成立，则`Acc r x`成立。
* 这本质上是一个“反向归纳”定义：要证明`Acc r x`，需先证明所有比`x`“更小”的元素（按`r`关系）也满足`Acc`。

=== 良基关系 ===
若对于所有`x : α`，`Acc r x`成立，则称`r`是一个'''良基关系'''（Well-founded relation）。良基关系保证了归纳和递归的合法性。

== 代码示例 ==

以下是一个简单的例子，展示如何使用`Acc`定义递归函数：

<syntaxhighlight lang="lean">
def ackermann : Nat → Nat → Nat :=
  WellFounded.fix (Nat.lt_wfRel.wf) -- 使用Nat上的<关系作为良基关系
    (λ m rec =>
      WellFounded.fix (Nat.lt_wfRel.wf) -- 嵌套递归，对n使用相同的良基关系
        (λ n rec' =>
          match m, n with
          | 0,   n   => n + 1
          | m+1, 0   => rec m 1 (by simp_arith)
          | m+1, n+1 => rec m (rec' n (by simp_arith)) (by simp_arith)))
</syntaxhighlight>

'''输入与输出示例'''：
* `ackermann 0 5` 输出 `6`
* `ackermann 3 1` 输出 `13`

解释：
* 这里使用`Nat.lt_wfRel.wf`（自然数上的`<`关系是良基的）来保证递归终止。
* `WellFounded.fix`是Lean提供的工具，用于基于`Acc`关系定义递归函数。

== 实际应用场景 ==

Acc关系的典型应用包括：
1. '''递归函数定义'''：如阿克曼函数、欧几里得算法等。
2. '''归纳证明'''：证明关于递归结构的命题时，使用`Acc`作为归纳依据。
3. '''自定义数据结构的递归'''：如树或图的遍历，其中需要显式指定终止条件。

=== 案例：列表的归并排序 ===
以下是一个简化的归并排序实现，使用`Acc`确保递归终止：

<syntaxhighlight lang="lean">
def mergeSort [DecidableLinearOrder α] : List α → List α :=
  WellFounded.fix (invImage length (Nat.lt_wfRel.wf)) -- 基于列表长度的<关系
    (λ xs rec =>
      match xs with
      | [] => []
      | [x] => [x]
      | _ =>
        let (l, r) := xs.splitAt (xs.length / 2)
        merge (rec l (by simp_arith)) (rec r (by simp_arith)))
</syntaxhighlight>

== 可视化：Acc关系的结构 ==

<mermaid>
graph TD
    A[Acc r x] --> B[∀ y, r y x → Acc r y]
    B --> C[Acc r y₁]
    B --> D[Acc r y₂]
    C --> E[∀ z, r z y₁ → Acc r z]
    D --> F[∀ z, r z y₂ → Acc r z]
</mermaid>

说明：该图展示了`Acc r x`的依赖结构，每个节点的可访问性依赖于其所有前驱节点的可访问性。

== 数学基础 ==

Acc关系的核心是良基归纳法。若`r`是良基的，则可使用以下归纳原理：
<math>
\frac{\forall x, (\forall y, r\,y\,x \to P\,y) \to P\,x}{\forall x, P\,x}
</math>

在Lean中，这对应于`Acc.rec`或`WellFounded.rec`。

== 常见问题 ==

1. '''如何选择良基关系？'''
   - 对于自然数，通常使用`<`。
   - 对于列表或树，可使用长度或深度作为度量。
   - 自定义关系需手动证明其良基性。

2. '''Lean如何自动推断Acc证明？'''
   - 通过类型类实例（如`Nat.lt_wfRel`）或用户提供的证明。

== 总结 ==

Acc关系是Lean中处理递归和归纳的基石。通过理解其定义和使用方法，用户可以安全地定义复杂的递归函数或进行深入的归纳证明。实际应用中，结合`WellFounded.fix`和适当的良基关系，能够覆盖绝大多数递归场景。

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