Lean协递归

Lean协递归（Coinduction in Lean）是函数式编程和定理证明中处理无限数据结构（如无限流、无限树等）的核心技术。与普通递归（处理有限数据）不同，协递归通过惰性求值和核心cursion原理定义可能无限的计算过程。本文将系统介绍Lean中协递归的理论、语法及实际应用。

基本概念

协递归是递归的对偶概念：

• 递归：从基本案例出发，通过有限步骤构造结果（如列表、自然数）。
• 协递归：通过观察和展开操作处理无限结构（如无限流、进程行为）。

数学上，协递归类型是终余代数（Final Coalgebra）的体现。例如，无限流类型 $\mathrm{S}\mathrm{t}\mathrm{r}\mathrm{e}\mathrm{a}\mathrm{m}\alpha \cong \alpha \times \mathrm{S}\mathrm{t}\mathrm{r}\mathrm{e}\mathrm{a}\mathrm{m}\alpha$ 的解是协递归定义的。

Lean中的协递归语法

Lean使用关键字 coinductive 定义协递归类型，并通过 corec 或 corecursive 定义函数。

协递归类型定义

定义一个表示二进制无限流的类型：

coinductive BinStream : Type
| cons (head : Nat) (tail : BinStream) : BinStream

协递归函数示例

生成一个无限常数流：

def constStream (n : Nat) : BinStream :=
  corec (λ _ => BinStream.cons n (constStream n))

执行观察操作（取前3个元素）：

-- 输出: [n, n, n, ...]
#eval (constStream 5).head  -- 5
#eval (constStream 5).tail.head  -- 5

核心原理

协递归的正确性依赖于：

1. 生产率（Productivity）：每次展开必须产生一个构造函数（如 cons）。
2. 守卫性（Guardedness）：递归调用必须被构造函数“保护”（如 tail 在 cons 内）。

守卫性检查示例

以下定义会被Lean拒绝（未满足守卫性）：

-- 错误：递归调用未受保护
def badStream : BinStream := corec (λ _ => badStream)

正确版本：

def ones : BinStream := corec (λ _ => BinStream.cons 1 ones)

实际应用案例

案例1：斐波那契无限流

coinductive FibStream : Type
| cons (a b : Nat) (next : FibStream) : FibStream

def fib : FibStream :=
  corec (λ (a, b) => FibStream.cons a b (fib (b, a + b))) (0, 1)

观察输出：

#eval fib.head           -- 0
#eval fib.next.head      -- 1
#eval fib.next.next.head -- 1

案例2：交互式进程建模

用协递归模拟一个响应式进程：

coinductive Process (α : Type) : Type
| step (output : α) (next : Process α) : Process α
| halt : Process α

def repeater (msg : String) : Process String :=
  corec (λ _ => Process.step msg (repeater msg))

与递归的对比

递归 vs 协递归

特性	递归	协递归
数据范围	有限	可能无限
终止性	必须终止	可能永不终止
Lean关键字	inductive	coinductive
典型应用	列表、树	流、状态机

高级主题：余模式匹配

Lean支持余模式匹配（Copattern Matching），通过观察行为定义协递归函数：

def zeros : BinStream
  | .head => 0
  | .tail => zeros

可视化：无限流结构

graph LR A[Stream.cons head=1] --> B[Stream.cons head=1] --> C[Stream.cons head=1] --> D[...]

常见错误与调试

• 错误：未满足生产率导致编译失败。

 * 解决：确保每次调用至少产生一个构造函数。

• 错误：意外严格求值导致堆栈溢出。

 * 解决：使用 Lazy 类型或 corec 关键字。

练习建议

1. 定义一个交替输出 true 和 false 的无限流。 2. 实现一个协递归的“映射”函数，对流的每个元素应用操作。 3. 证明两个无限流的外延等价性（使用 bisimulation）。

总结

Lean协递归为处理无限数据结构提供了类型安全的工具，关键在于理解守卫性和生产率。通过惰性求值，我们能够高效地建模现实中的无限过程（如传感器数据、游戏状态等）。