Lean测度函数

简介[编辑 | 编辑源代码]

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

在Lean中，测度函数通常表现为：

将输入参数映射到自然数的函数
满足每次递归调用时测度值严格递减
通过well-founded recursion原则保证终止性

数学基础[编辑 | 编辑源代码]

测度函数的理论基础建立在良基关系（well-founded relation）上。对于类型 $α$ ，若存在关系 $R : α \to α \to P r o p$ 满足： $\forall S \subseteq α, S \neq \emptyset ⟹ \exists m \in S, \forall x \in S, \neg R x m$

则称 $R$ 是良基关系。测度函数 $m : α \to ℕ$ 诱导的良基关系为： $x ≺ y ⟺ m x < m y$

基本语法[编辑 | 编辑源代码]

在Lean4中，使用`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)

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

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

案例1：列表分割[编辑 | 编辑源代码]

考虑一个将列表分成两半的函数：

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

解释：

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

案例2：归并排序[编辑 | 编辑源代码]

更复杂的测度函数应用：

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

分析：

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

高级主题[编辑 | 编辑源代码]

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

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

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猜想未解决）

多参数测度[编辑 | 编辑源代码]

处理相互递归函数时：

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