跳转到内容

Lean终止性证明：修订间差异

来自代码酷
可视化wikitext
Admin​（留言 | 贡献）
行政员、​界面管理员、​管理员
8,039次编辑
Page creation by admin bot
 
Admin​（留言 | 贡献）
行政员、​界面管理员、​管理员
8,039次编辑
Page update by admin bot
 
第1行： 第1行：
= Lean终止性证明 =
= Lean终止性证明 =


'''终止性证明'''（Termination Proof）是形式化验证中确保递归函数或循环结构最终会停止执行的重要技术。在Lean定理证明器中，终止性证明通过结构归纳、良基关系或度量函数等方式实现，是构建可靠数学软件和验证程序正确性的核心工具。
'''终止性证明'''是Lean定理证明器中对递归函数或归纳定义进行验证的关键技术，它确保函数在所有可能的输入下都能在有限步骤内停止计算。本文将从基础概念到实际应用全面介绍Lean中的终止性证明方法。


== 基本概念 ==
== 基本概念 ==


在编程语言理论中，一个函数若满足以下条件则称为'''终止的'''：
在Lean中，所有函数必须是'''全函数'''（total functions），这意味着它们必须在所有合法输入上终止。这与某些编程语言允许部分函数（可能无限循环）的设计哲学不同。
* 对于所有有效的输入，函数执行过程会在有限步骤内返回结果。
* 不会进入无限循环或发散状态。


Lean使用类型系统和依赖类型强制要求所有定义的函数必须具有终止性证明。这与常规编程语言（如Python或Java）有本质区别——后者允许非终止函数的定义。
终止性证明的核心思想是：
* 每次递归调用时，函数的某个参数必须'''严格递减'''
* 这种递减关系必须满足'''良基关系'''（well-founded relation）


=== 为什么需要终止性证明？ ===
数学表达为：对于递归调用 <math>f(y)</math> 和当前参数 <math>x</math>，必须满足 <math>y \prec x</math>，其中 <math>\prec</math> 是良基关系。
* '''逻辑一致性'''：非终止函数可能导致逻辑矛盾（如无限递归可推导出任意命题）
* '''可计算性保证'''：确保函数在所有输入下都能给出结果
* '''资源控制'''：避免程序运行时出现不可预测的无限消耗


== 终止性证明机制 ==
== 基础示例 ==


Lean主要通过两种方式验证终止性：
最简单的例子是自然数上的递归函数：
 
=== 1. 结构递归 ===
当函数参数在递归调用时严格"变小"（按某种良序关系），Lean可自动识别终止性。例如自然数的结构归纳：


<syntaxhighlight lang="lean">
<syntaxhighlight lang="lean">
def factorial : Nat → Nat
def factorial : Nat → Nat
  | 0 => 1
| 0 => 1
  | n+1 => (n+1) * factorial n -- 递归参数从n+1变为n
| n+1 => (n+1) * factorial n
</syntaxhighlight>
</syntaxhighlight>


'''验证过程'''：
Lean会自动识别：
1. Lean检测到递归调用时参数从`n+1`变为`n`
1. 模式匹配将参数从<code>n+1</code>降到<code>n</code>
2. 自然数满足`n < n+1`的良序关系
2. 自然数的<code><</code>关系是良基的
3. 系统自动接受该定义
 
== 复杂情况处理 ==
 
当自动推断失败时，需要显式提供终止证明。常见方法有：


=== 2. 使用`termination_by`指令 ===
=== 使用<code>termination_by</code>===
对于复杂情况，需显式指定终止度量。例如阿克曼函数：


<syntaxhighlight lang="lean">
<syntaxhighlight lang="lean">
def ackermann : Nat → Nat → Nat
def ackermann : Nat → Nat → Nat
  | 0, n => n + 1
| 0, n => n + 1
  | m+1, 0 => ackermann m 1
| m+1, 0 => ackermann m 1
  | m+1, n+1 => ackermann m (ackermann (m+1) n)
| m+1, n+1 => ackermann m (ackermann (m+1) n)
termination_by m n => (m, n)  -- 按字典序比较二元组
termination_by ackermann m n => (m, n)  -- 按字典序递减
</syntaxhighlight>
 
这里我们指定按字典序比较二元组<code>(m,n)</code>。
 
=== 使用<code>decreasing_by</code>===
 
当需要更复杂的证明时：
 
<syntaxhighlight lang="lean">
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决策过程
</syntaxhighlight>
</syntaxhighlight>


'''度量函数原理'''：
== 良基关系 ==
 
Lean中预定义的良基关系包括：
 
<mermaid>
<mermaid>
graph TD
graph TD
     A[调用ackermann m n] -->|m减小或m不变n减小| B[终止性保证]
     A[WellFoundedRelation] --> B[Nat.lt]
     B --> C[字典序 (m,n) < (m+1,n+1)]
     A --> C[List.length]
    A --> D[Prod.Lex]
    D --> E[字典序]
    A --> F[InvImage]
</mermaid>
</mermaid>


== 实际案例 ==
自定义类型的良基关系需要构造：
 
=== 案例1：列表处理的终止性 ===
处理列表时需保证递归调用作用于更短的子列表：


<syntaxhighlight lang="lean">
<syntaxhighlight lang="lean">
def listSum : List Nat → Nat
inductive Tree where
  | [] => 0
   | node (children : List Tree)
   | x :: xs => x + listSum xs  -- xs是原列表的严格子结构
</syntaxhighlight>


=== 案例2：复杂终止条件的证明 ===
def Tree.height : Tree → Nat
欧几里得算法需要自定义终止度量：
  | .node ts => 1 + (ts.map height).maximumD 0


<syntaxhighlight lang="lean">
instance : WellFoundedRelation Tree where
def gcd : Nat → Nat → Nat
   rel := fun t1 t2 => height t1 < height t2
   | 0, n => n
   wf := sorry -- 证明省略
  | m, 0 => m
   | m+1, n+1 =>
      if m < n then
        gcd (m+1) (n - m - 1)
      else
        gcd (m - n) (n+1)
termination_by m n => m + n -- 总和严格递减
</syntaxhighlight>
</syntaxhighlight>


'''终止性分析'''：
== 实际应用案例 ==
* 每次递归调用：`m + n`的值至少减少1
* 当`m + n = 0`时达到基本情况
* 因此函数必然终止


== 高级技巧 ==
=== 归并排序 ===
 
=== 良基关系（Well-founded Relation） ===
对于无法简单度量的情况，可构造良基关系证明终止。例如处理树形结构：


<syntaxhighlight lang="lean">
<syntaxhighlight lang="lean">
inductive Tree (α : Type) where
def mergeSort [Ord α] (xs : List α) : List α :=
   | leaf : α → Tree α
   let n := xs.length
   | node : List (Tree α) → Tree α
   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
</syntaxhighlight>


def treeDepth : Tree α → Nat
终止性证明依赖于列表长度的递减：
  | .leaf _ => 1
1. <code>left.length < xs.length</code>
  | .node ts =>  
2. <code>right.length < xs.length</code>
      1 + (ts.map treeDepth).maximum  -- 递归作用于严格子树
</syntaxhighlight>


此时Lean自动识别`ts`是原树的严格子树，满足树结构的良基关系。
=== 计算游戏步骤 ===


=== 非显然终止的证明 ===
考虑一个每次将数字减半或减一的游戏：
某些算法（如合并排序）需要更复杂的终止论证：


<syntaxhighlight lang="lean">
<syntaxhighlight lang="lean">
def mergeSort [Ord α] (xs : List α) : List α :=
def gameStep : Nat → Nat
  let mid := xs.length / 2
| 0 => 0
   if mid = 0 then xs
| n =>
   else  
   if n % 2 == 0 then
     merge
    gameStep (n / 2)
      (mergeSort (xs.take mid))  -- 长度mid < length xs
   else
      (mergeSort (xs.drop mid)) -- 长度length xs - mid < length xs
     gameStep (n - 1)
termination_by xs.length
termination_by gameStep n => n
</syntaxhighlight>
</syntaxhighlight>


'''关键观察'''：
== 常见问题与解决 ==
* 使用`termination_by`显式指定列表长度作为度量
 
* 数学性质保证：`0 < mid → mid < length xs`和`length xs - mid < length xs`
'''问题1'''：非结构递归如何证明？
* 解决方案：使用<code>WellFounded.fix</code>和自定义关系


== 常见错误与解决方案 ==
'''问题2'''：相互递归函数如何处理？
* 解决方案：使用<code>mutual</code>块并联合证明


{| class="wikitable"
<syntaxhighlight lang="lean">
|+ 终止性证明问题排查
mutual
! 错误类型 !! 示例 !! 解决方法
def even : Nat → Bool
|-
| 0 => true
| 非结构递归 | <code>def f x := f (x + 1)</code> | 添加递减度量如<code>termination_by 100 - x</code>
| n+1 => odd n
|-
| 多参数复杂依赖 | <code>def f x y := f (y-1) (x+1)</code> | 使用字典序：<code>termination_by x y => (x+y, x)</code>
|-
| 嵌套递归 | <code>def f x := f (f (x-1))</code> | 证明内层调用不增加原始参数大小
|}


== 数学基础 ==
def odd : Nat → Bool
| 0 => false
| n+1 => even n
end
</syntaxhighlight>


终止性证明的理论基础是'''良基归纳法'''：
== 进阶话题 ==
<math>
\forall x, (\forall y \prec x, P(y)) \to P(x) \implies \forall x, P(x)
</math>
其中<math>\prec</math>是集合上的良基关系（即不存在无限递减链）。


在Lean中，该原理通过`WellFoundedRelation`类型类实现，所有内置类型（如Nat, List, Tree等）都已配备默认的良基关系。
对于高级用户，Lean支持：
* 使用<code>measure</code>指定任意度量函数
* 通过<code>Finset</code>证明有限性
* 使用<code>WellFounded.fix</code>手动构造递归


== 练习建议 ==
== 总结 ==


1. 尝试将非终止的Python递归函数转换为Lean中的终止版本
Lean的终止性证明机制确保了：
2. 为二分查找算法编写终止性证明
* 所有函数都是全函数
3. 设计一个需要自定义`WellFoundedRelation`的复杂数据结构
* 递归定义在逻辑上一致
* 可以通过多种方式适应不同场景


通过系统练习，读者可以深入理解如何构建可靠的终止性论证，这是形式化验证和函数式编程的核心技能之一。
掌握这些技术对于在Lean中编写正确的递归算法和归纳定义至关重要。初学者应从简单示例开始，逐步理解良基关系和终止证明的构造方法。


[[Category:计算机科学]]
[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean]]
[[Category:Lean程序验证]]
[[Category:Lean归纳与递归]]

2025年5月12日 (一) 00:30的最新版本

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中预定义的良基关系包括：

graph TD A[WellFoundedRelation] --> B[Nat.lt] A --> C[List.length] A --> D[Prod.Lex] D --> E[字典序] A --> F[InvImage]

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

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中编写正确的递归算法和归纳定义至关重要。初学者应从简单示例开始，逐步理解良基关系和终止证明的构造方法。

检索自“https://wiki.echo.cool/index.php?title=Lean终止性证明&oldid=22428”