编辑“︁Lean互递归定义”︁

`= Lean互递归定义 =`

互递归（Mutual Recursion）是函数式编程中一种重要的递归形式，指两个或多个函数相互调用形成的递归结构。在Lean定理证明器中，互递归定义允许我们同时定义多个相互依赖的函数或数据类型。

== 基本概念 ==

互递归的核心特征是'''定义项的相互依赖'''。例如：
* 函数A的定义中包含对函数B的调用
* 函数B的定义中包含对函数A的调用
* 这种相互调用形成递归结构

在Lean中，互递归定义需要使用`mutual`关键字明确声明。与普通递归不同，互递归要求所有相关定义必须'''同时给出'''，因为它们的正确性相互依赖。

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

这个经典示例展示了如何用互递归判断奇偶数：
* `isEven`函数依赖`isOdd`的结果
* `isOdd`函数依赖`isEven`的结果
* 通过`mutual`块将两者绑定为一个定义单元

== 语法结构 ==

Lean中的互递归定义遵循特定语法：

<syntaxhighlight lang="lean">
mutual
  <定义1>
  <定义2>
  ...
  <定义n>
end
</syntaxhighlight>

关键限制：
1. 所有互递归定义必须放在同一个`mutual`块中
2. 块内定义的顺序不影响语义
3. 必须保证所有递归调用都是'''结构递归'''（即参数向基准情形收敛）

== 数据类型互递归 ==

互递归不仅适用于函数，也可用于定义相互依赖的数据类型：

<syntaxhighlight lang="lean">
mutual
  inductive Even where
    | zero : Even
    | succ : Odd → Even
  
  inductive Odd where
    | succ : Even → Odd
end
</syntaxhighlight>

这个定义建立了两种类型的互递归关系：
* `Even`类型包含从`Odd`构造的值
* `Odd`类型包含从`Even`构造的值

== 终止性证明 ==

Lean要求所有递归函数必须可证明终止。对于互递归函数，终止性证明需要特殊处理。常见方法：

1. '''使用`termination_by`子句'''：明确指定测度函数
2. '''依赖类型技巧'''：通过类型系统保证终止

示例：

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

这里`termination_by`指定按字典序比较参数的元组。

== 实际应用案例 ==

=== 语法树处理 ===

互递归非常适合处理嵌套的语法结构：

<syntaxhighlight lang="lean">
mutual
  def evalExpr : Expr → Option Value
    | Expr.num n => some (Value.num n)
    | Expr.plus e1 e2 => 
      match (evalExpr e1, evalExpr e2) with
      | (some (Value.num n1), some (Value.num n2)) => some (Value.num (n1 + n2))
      | _ => none
  
  def evalStmt : Stmt → Env → Option Env
    | Stmt.assign x e, env =>
      match evalExpr e with
      | some v => some (env.insert x v)
      | none => none
end
</syntaxhighlight>

=== 状态机建模 ===

互递归可以清晰表达状态转换：

<mermaid>
stateDiagram-v2
    [*] --> Even
    Even --> Odd: succ
    Odd --> Even: succ
</mermaid>

对应实现：

<syntaxhighlight lang="lean">
mutual
  def nextEven : Even → Odd := fun
    | Even.zero => Odd.succ (Even.succ Even.zero)
    | Even.succ o => Odd.succ (Even.succ o)
  
  def nextOdd : Odd → Even := fun
    | Odd.succ e => Even.succ (nextEven e)
end
</syntaxhighlight>

== 常见问题与解决方案 ==

'''问题1'''：非结构递归导致终止性证明失败
* 解决方案：重构为结构递归或提供显式测度函数

'''问题2'''：互递归定义过于复杂
* 解决方案：考虑使用嵌套定义或辅助函数简化

'''问题3'''：类型推断困难
* 解决方案：添加显式类型注解

== 数学基础 ==

互递归的理论基础是'''互递归定理'''（Mutual Recursion Theorem），它保证了在满足一定条件时，互递归定义是良定的。形式化地，给定函数方程组：

<math>
\begin{cases}
f_1(x) = F_1(f_1,...,f_n,x) \\
\vdots \\
f_n(x) = F_n(f_1,...,f_n,x)
\end{cases}
</math>

当所有<math>F_i</math>都是收缩映射时，方程有唯一解。

== 高级技巧 ==

对于复杂场景，可以结合以下技术：
* '''嵌套互递归'''：`mutual`块内包含另一个`mutual`
* '''参数化互递归'''：定义带参数的互递归函数族
* '''互递归定理'''：使用`mutual`定义定理组

示例：

<syntaxhighlight lang="lean">
mutual
  theorem even_add (m n : Nat) : isEven (m + n) = (isEven m == isEven n) := by
    induction m with
    | zero => simp [isEven]
    | succ m ih => simp [isEven, odd_add, ih]
  
  theorem odd_add (m n : Nat) : isOdd (m + n) = (isOdd m != isOdd n) := by
    induction m with
    | zero => simp [isOdd]
    | succ m ih => simp [isOdd, even_add, ih]
end
</syntaxhighlight>

== 总结 ==

互递归是Lean中表达相互依赖计算的强大工具，特点包括：
1. 必须使用`mutual`块明确声明
2. 适用于函数和数据类型定义
3. 需要特别注意终止性证明
4. 在语法处理、状态机等场景特别有用

正确使用互递归可以大幅简化复杂相互依赖关系的表达，使代码更符合数学直觉。

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