编辑“︁Lean程序提取”︁

{{DISPLAYTITLE:Lean程序提取}}

== 简介 ==
'''Lean程序提取'''（Program Extraction）是Lean定理证明器中一项重要功能，允许用户从形式化证明或构造性定义中提取可执行的程序代码。这一过程基于'''柯里-霍华德同构'''（Curry-Howard correspondence），将数学证明转化为计算内容。提取的代码通常具有高度可靠性，因为它直接源于经过验证的规范。

程序提取的核心价值在于：
* 通过形式化验证保证程序正确性
* 自动生成高效可执行代码（如OCaml、C或JavaScript）
* 支持从抽象规范到具体实现的转换

== 基本原理 ==
在Lean中，程序提取依赖于构造性逻辑。当用户完成一个构造性证明或定义时，Lean可以将其内容转换为目标语言的代码。提取过程遵循以下逻辑关系：

<mermaid>
graph LR
    A[形式化规范] -->|构造性证明| B(Lean项)
    B -->|提取| C[可执行代码]
    C --> D{目标语言}
    D --> E[OCaml]
    D --> F[C]
    D --> G[JavaScript]
</mermaid>

数学上，这对应于类型论中的提取规则：
<math>
\frac{\Gamma \vdash t : T \quad \text{T是可提取类型}}{\text{extract}(t) : \text{目标语言}}
</math>

== 基础示例 ==
以下是一个简单的自然数加法定义及其提取示例：

<syntaxhighlight lang="lean">
-- Lean定义
def natAdd : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.succ (natAdd n m)

-- 提取命令
#eval natAdd 2 3  -- 输出: 5
</syntaxhighlight>

当使用`#print`命令时，可以看到Lean内部表示：
<syntaxhighlight lang="lean">
#print natAdd
-- 输出:
-- def natAdd : Nat → Nat → Nat :=
-- fun n m => Nat.recOn m n fun m' ih => Nat.succ ih
</syntaxhighlight>

提取到OCaml的代码可能如下：
<syntaxhighlight lang="ocaml">
let rec natAdd n = function
  | O -> n
  | S m -> S (natAdd n m)
</syntaxhighlight>

== 高级特性 ==
=== 依赖类型的提取 ===
Lean支持从依赖类型中提取代码。以下示例展示了一个长度索引向量：

<syntaxhighlight lang="lean">
inductive Vec (α : Type) : Nat → Type where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)

def head {α : Type} : Vec α (n+1) → α
  | cons x xs => x

-- 提取时会自动擦除无关的类型参数
</syntaxhighlight>

提取结果将忽略类型级自然数参数，仅保留运行时必要的部分。

=== 证明无关性 ===
Lean使用'''证明无关性'''（Proof Irrelevance）原则，在提取时会删除纯证明项。例如：

<syntaxhighlight lang="lean">
def extractExample (x : Nat) (h : x = x) : Nat :=
  x + 1

-- 提取后的代码将忽略h参数
</syntaxhighlight>

OCaml输出：
<syntaxhighlight lang="ocaml">
let extractExample x _ = x + 1
</syntaxhighlight>

== 实际应用案例 ==
=== 排序算法验证 ===
考虑一个经过形式化验证的快速排序实现：

<syntaxhighlight lang="lean">
def qsort : List Nat → List Nat
  | [] => []
  | x::xs =>
    let (lo, hi) := xs.partition (· ≤ x)
    qsort lo ++ [x] ++ qsort hi

theorem qsort_sorted (l : List Nat) : (qsort l).Sorted :=
  -- 验证证明省略...

-- 提取后可获得已验证的排序实现
</syntaxhighlight>

=== 密码学原语 ===
在密码学中，程序提取可以保证实现的正确性：

<syntaxhighlight lang="lean">
def SHA256 (msg : List UInt8) : List UInt8 :=
  -- 形式化定义的哈希函数
  ...

theorem collision_resistance : ∀ m1 m2,
    SHA256 m1 = SHA256 m2 → m1 = m2 :=
  -- 安全性证明
  ...
</syntaxhighlight>

== 提取控制 ==
用户可以通过以下方式控制提取过程：

{| class="wikitable"
! 指令 !! 作用
|-
| <code>@[export]</code> || 强制导出特定定义
|-
| <code>@[inline]</code> || 提示编译器内联函数
|-
| <code>@[noextract]</code> || 阻止定义被提取
|}

示例：
<syntaxhighlight lang="lean">
@[export myadd]
def specialAdd (x y : Nat) := x + y
</syntaxhighlight>

== 限制与注意事项 ==
1. '''经典逻辑限制'''：使用经典公理（如选择公理）的部分无法提取
2. '''宇宙限制'''：Type u等高宇宙层级内容可能被简化
3. '''IO处理'''：需要显式标记IO操作用于提取

错误示例：
<syntaxhighlight lang="lean">
-- 这将无法提取，因为使用了经典选择
noncomputable def badExample : Nat → Nat :=
  fun x => Classical.choose (exists_eq_add x)
</syntaxhighlight>

== 最佳实践 ==
* 明确标记需要提取的定义
* 为关键函数编写形式化规范
* 使用<code>#eval</code>测试提取前的行为
* 保持构造性定义风格

== 进阶主题 ==
=== 自定义提取后端 ===
高级用户可以扩展Lean提取系统，添加对新目标语言的支持。这需要：
1. 实现新的代码生成器
2. 注册提取翻译规则
3. 处理目标语言特定特性

=== 部分提取 ===
通过<code>partial</code>关键字可以提取非终止计算：

<syntaxhighlight lang="lean">
partial def fib (n : Nat) : Nat :=
  if n ≤ 1 then n else fib (n-1) + fib (n-2)
</syntaxhighlight>

== 参见 ==
* 构造性数学
* 代码生成技术
* 形式化验证

== 总结 ==
Lean程序提取将形式化验证与实际编程连接起来，使得：
* 理论证明可以转化为可靠实现
* 减少传统开发中的测试负担
* 支持多语言目标输出
通过掌握这一技术，开发者可以构建高可信度的软件系统。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean程序验证]]