编辑“︁Lean测度函数”︁

{{DISPLAYTITLE:Lean测度函数}}

== 简介 ==
'''Lean测度函数'''是Lean定理证明器中用于处理递归定义的重要工具，它通过数学上的'''测度（measure）'''概念确保递归函数的终止性。在依赖类型理论中，所有函数必须被证明是'''全函数（total function）'''，而测度函数提供了结构归纳之外的另一种终止性证明方法。

在Lean中，测度函数通常表现为：
* 将输入参数映射到自然数的函数
* 满足每次递归调用时测度值严格递减
* 通过'''well-founded recursion'''原则保证终止性

== 数学基础 ==
测度函数的理论基础建立在'''良基关系（well-founded relation）'''上。对于类型<math>\alpha</math>，若存在关系<math>R : \alpha \to \alpha \to \mathsf{Prop}</math>满足：
<math>
\forall S \subseteq \alpha, S \neq \emptyset \implies \exists m \in S, \forall x \in S, \neg R\ x\ m
</math>

则称<math>R</math>是良基关系。测度函数<math>m : \alpha \to \mathbb{N}</math>诱导的良基关系为：
<math>
x \prec y \iff m\ x < m\ y
</math>

== 基本语法 ==
在Lean4中，使用`termination_by`子句指定测度函数：

<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

这个例子展示了：
1. 著名的阿克曼函数定义
2. 使用二元组<code>(m, n)</code>作为测度
3. Lean会自动按字典序比较元组来证明终止性

== 实际案例 ==
=== 案例1：列表分割 ===
考虑一个将列表分成两半的函数：

<syntaxhighlight lang="lean">
def splitList (xs : List α) : List α × List α :=
  match xs with
  | [] => ([], [])
  | [x] => ([x], [])
  | x::y::zs =>
    let (l, r) := splitList zs
    (x::l, y::r)
termination_by splitList xs => xs.length
</syntaxhighlight>

'''解释'''：
* 测度函数选择<code>xs.length</code>
* 每次递归时<code>zs.length < xs.length</code>成立
* 输出示例：<code>splitList [1,2,3,4] = ([1,3], [2,4])</code>

=== 案例2：归并排序 ===
更复杂的测度函数应用：

<syntaxhighlight lang="lean">
def mergeSort [Ord α] (xs : List α) : List α :=
  if xs.length ≤ 1 then xs
  else
    let mid := xs.length / 2
    let (l, r) := xs.splitAt mid
    merge (mergeSort l) (mergeSort r)
termination_by mergeSort xs => xs.length
</syntaxhighlight>

'''分析'''：
* 测度函数同样是列表长度
* 关键性质：<code>l.length < xs.length ∧ r.length < xs.length</code>
* 使用<code>splitAt</code>确保子列表严格变小

== 高级主题 ==
=== 自定义良基关系 ===
当自然数测度不够时，可以定义完全自定义的良基关系：

<syntaxhighlight lang="lean">
def f (x : Nat) : Nat :=
  if x = 0 then 1
  else if x % 2 = 0 then f (x / 2)
  else f (3 * x + 1)
termination_by f x => x
decreasing_by
  simp_wf  -- 自动生成递减证明
  sorry    -- 实际应用中需补充证明（Collatz猜想未解决）
</syntaxhighlight>

=== 多参数测度 ===
处理相互递归函数时：

<syntaxhighlight lang="lean">
mutual
def even : Nat → Bool
  | 0 => true
  | n+1 => odd n
def odd : Nat → Bool
  | 0 => false
  | n+1 => even n
end
termination_by
  even n => n
  odd n => n
</syntaxhighlight>

== 可视化 ==
阿克曼函数的测度变化可以用mermaid表示：

<mermaid>
graph TD
    A["ack(2,2)"] --> B["ack(1, ack(2,1))"]
    B --> C["ack(2,1)"]
    C --> D["ack(1, ack(2,0))"]
    D --> E["ack(2,0)"]
    E --> F["ack(1,1)"]
    F --> G["ack(0, ack(1,0))"]
    G --> H["ack(1,0)"]
    H --> I["ack(0,1)"]
</mermaid>

== 常见问题 ==
'''Q: 如何选择测度函数？'''
* 优先选择能直接反映问题规模的参数（如列表长度、树高度）
* 对于复杂递归，可能需要构造合成测度（如元组、和类型）

'''Q: Lean如何验证测度有效性？'''
* 自动生成递减义务（decreasing proof obligation）
* 需要证明每次递归调用时测度严格递减
* 可使用<code>decreasing_by</code>子句提供显式证明

== 最佳实践 ==
1. '''保持简单'''：优先使用结构归纳，仅在必要时用测度函数
2. '''模块化'''：将复杂递归分解为多个简单函数
3. '''文档化'''：用注释说明测度函数的设计意图
4. '''测试'''：用极端案例验证终止性（如空列表、极大输入等）

== 延伸阅读 ==
* 良基递归的数学理论
* Lean核心库中的测度函数应用（如<code>Array.qsort</code>）
* 与结构归纳法的比较研究

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