Lean终止性证明[编辑 | 编辑源代码]

终止性证明是Lean定理证明器中对递归函数或归纳定义进行验证的关键技术，它确保函数在所有可能的输入下都能在有限步骤内停止计算。本文将从基础概念到实际应用全面介绍Lean中的终止性证明方法。

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

在Lean中，所有函数必须是全函数（total functions），这意味着它们必须在所有合法输入上终止。这与某些编程语言允许部分函数（可能无限循环）的设计哲学不同。

终止性证明的核心思想是：

每次递归调用时，函数的某个参数必须严格递减
这种递减关系必须满足良基关系（well-founded relation）

数学表达为：对于递归调用 $f (y)$ 和当前参数 $x$ ，必须满足 $y ≺ x$ ，其中 $≺$ 是良基关系。

基础示例[编辑 | 编辑源代码]

最简单的例子是自然数上的递归函数：

def factorial : Nat → Nat
| 0 => 1
| n+1 => (n+1) * factorial n

Lean会自动识别： 1. 模式匹配将参数从n+1降到n 2. 自然数的<关系是良基的

复杂情况处理[编辑 | 编辑源代码]

当自动推断失败时，需要显式提供终止证明。常见方法有：

使用`termination_by`[编辑 | 编辑源代码]

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)  -- 按字典序递减

这里我们指定按字典序比较二元组(m,n)。

使用`decreasing_by`[编辑 | 编辑源代码]

当需要更复杂的证明时：

def gcd : Nat → Nat → Nat
| 0, n => n
| m, 0 => m
| m+1, n+1 =>
  if m < n then
    gcd (m+1) (n - m - 1)
  else
    gcd (m - n - 1) (n+1)
termination_by _ m n => (m, n)
decreasing_by
  simp_wf  -- 清理目标
  try apply Prod.Lex.right
  try apply Prod.Lex.left
  all_goals omega  -- 使用omega决策过程

良基关系[编辑 | 编辑源代码]

Lean中预定义的良基关系包括：

自定义类型的良基关系需要构造：

inductive Tree where
  | node (children : List Tree)

def Tree.height : Tree → Nat
  | .node ts => 1 + (ts.map height).maximumD 0

instance : WellFoundedRelation Tree where
  rel := fun t1 t2 => height t1 < height t2
  wf := sorry  -- 证明省略

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

归并排序[编辑 | 编辑源代码]

def mergeSort [Ord α] (xs : List α) : List α :=
  let n := xs.length
  if h : n ≤ 1 then
    xs
  else
    let m := n / 2
    let (left, right) := xs.splitAt m
    merge (mergeSort left) (mergeSort right)
termination_by mergeSort xs => xs.length

终止性证明依赖于列表长度的递减： 1. left.length < xs.length 2. right.length < xs.length

计算游戏步骤[编辑 | 编辑源代码]

考虑一个每次将数字减半或减一的游戏：

def gameStep : Nat → Nat
| 0 => 0
| n =>
  if n % 2 == 0 then
    gameStep (n / 2)
  else
    gameStep (n - 1)
termination_by gameStep n => n

常见问题与解决[编辑 | 编辑源代码]

问题1：非结构递归如何证明？

解决方案：使用WellFounded.fix和自定义关系

问题2：相互递归函数如何处理？

解决方案：使用mutual块并联合证明

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

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

进阶话题[编辑 | 编辑源代码]

对于高级用户，Lean支持：

使用measure指定任意度量函数
通过Finset证明有限性
使用WellFounded.fix手动构造递归

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

Lean的终止性证明机制确保了：

所有函数都是全函数
递归定义在逻辑上一致
可以通过多种方式适应不同场景

掌握这些技术对于在Lean中编写正确的递归算法和归纳定义至关重要。初学者应从简单示例开始，逐步理解良基关系和终止证明的构造方法。