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`是一个归纳定义的谓词，其定义如下：

inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
  | intro (x : α) (h : ∀ y, r y x → Acc r y) : Acc r x

解释：

• `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`定义递归函数：

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

输入与输出示例：

• `ackermann 0 5` 输出 `6`
• `ackermann 3 1` 输出 `13`

解释：

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

实际应用场景

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

案例：列表的归并排序

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

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

可视化：Acc关系的结构

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]

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

数学基础

Acc关系的核心是良基归纳法。若`r`是良基的，则可使用以下归纳原理： $\frac{\mathrm{\forall }x,(\mathrm{\forall }y,ryx\to Py)\to Px}{\mathrm{\forall }x,Px}$

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

常见问题

1. 如何选择良基关系？

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

2. Lean如何自动推断Acc证明？

  - 通过类型类实例（如`Nat.lt_wfRel`）或用户提供的证明。

总结

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