编辑“︁Lean函数理论”︁（章节）

= Lean函数理论 =

== 简介 ==
'''Lean函数理论'''是Lean定理证明器中处理函数定义、性质和应用的核心数学基础。作为依赖类型理论的一部分，它允许程序员以数学严谨的方式构造和操作函数。本章将系统讲解函数在Lean中的表示方式、高阶函数特性、柯里化等重要概念，并通过实际案例展示其在程序验证中的应用。

== 函数的基本定义 ==
在Lean中，函数使用'''λ表达式'''或'''箭头类型'''定义。基本语法遵循类型理论中的<math>\Pi</math>-类型（依赖乘积类型）规则：

<syntaxhighlight lang="lean">
-- 简单函数定义
def add_one : ℕ → ℕ := λ x, x + 1

-- 等价的多参数柯里化形式
def add : ℕ → ℕ → ℕ := λ x y, x + y
</syntaxhighlight>

'''关键特征：'''
* 所有函数默认是'''纯函数'''（无副作用）
* 参数类型和返回值类型必须显式声明
* 使用<code>→</code>符号表示非依赖函数类型

=== 类型推断 ===
Lean支持局部类型推断，但推荐显式注解类型以增强可读性：
<syntaxhighlight lang="lean">
-- 类型推断示例
#check λ (x : ℕ), x + 3  -- 输出：ℕ → ℕ
</syntaxhighlight>

== 高阶函数 ==
Lean中的函数可以作为参数和返回值，这是'''高阶函数'''的特性：

<syntaxhighlight lang="lean">
-- 接受函数作为参数
def apply_twice (f : ℕ → ℕ) (x : ℕ) : ℕ := f (f x)

-- 返回函数的函数
def compose (f g : ℕ → ℕ) : ℕ → ℕ := λ x, f (g x)
</syntaxhighlight>

'''应用实例：'''
<mermaid>
graph LR
    A[输入x] --> B[函数g]
    B --> C[中间结果]
    C --> D[函数f]
    D --> E[最终结果]
</mermaid>

== 依赖函数类型 ==
当返回值类型依赖输入值时，需要使用'''依赖乘积类型'''（Π-type）：

<syntaxhighlight lang="lean">
-- 依赖函数示例
def vector_repeat {α : Type} (n : ℕ) (x : α) : vector α n :=
vector.repeat x n
</syntaxhighlight>

此处<code>vector α n</code>的类型依赖于参数<code>n</code>的值。

== 定理证明中的应用 ==
函数理论在定理证明中体现为'''命题即类型'''原则：

<math>
\forall x \in A, P(x) \quad \text{对应} \quad \Pi x : A, P(x)
</math>

'''案例：交换性证明'''
<syntaxhighlight lang="lean">
theorem add_comm : ∀ (a b : ℕ), a + b = b + a :=
begin
  intros a b,
  induction b,
  { simp },
  { simp [nat.succ_add, b_ih] }
end
</syntaxhighlight>

== 递归与模式匹配 ==
Lean支持通过模式匹配定义递归函数：

<syntaxhighlight lang="lean">
-- 斐波那契数列
def fib : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := fib (n+1) + fib n
</syntaxhighlight>

'''终止性检查：'''
Lean会验证递归函数的终止性，防止无限递归。

== 部分应用与柯里化 ==
函数的部分应用是Lean的核心特性：

<syntaxhighlight lang="lean">
def add_five := add 5  -- 类型：ℕ → ℕ
#eval add_five 3       -- 输出：8
</syntaxhighlight>

柯里化的数学表示：
<math>
\text{add} : \mathbb{N} \to (\mathbb{N} \to \mathbb{N})
</math>

== 实际应用案例 ==
'''案例1：列表映射'''
<syntaxhighlight lang="lean">
def map_list (f : ℕ → ℕ) : list ℕ → list ℕ
| [] := []
| (h :: t) := f h :: map_list t
</syntaxhighlight>

'''案例2：微分近似'''
<syntaxhighlight lang="lean">
def derivative (f : ℝ → ℝ) (x ε : ℝ) : ℝ :=
(f (x + ε) - f x) / ε
</syntaxhighlight>

== 常见问题 ==
{| class="wikitable"
|-
! 问题 !! 解决方案
|-
| 函数应用时报类型错误 || 检查参数顺序和类型注解
|-
| 递归函数无法通过终止检查 || 添加递减参数或使用well-founded递归
|-
| 高阶函数难以调试 || 使用<code>#print</code>命令查看函数定义
|}

== 进阶主题 ==
* '''函数外延性公理'''：<code>f = g ↔ ∀ x, f x = g x</code>
* '''单子与函数组合'''：使用<code>>=></code>操作符
* '''异构计算'''：通过函数抽象实现跨领域验证

== 总结 ==
Lean函数理论为形式化数学和程序验证提供了坚实基础。通过：
1. 严格的类型系统保证正确性
2. 高阶函数实现抽象复用
3. 依赖类型表达复杂约束
开发者可以构建经数学验证的可靠系统。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数学基础]]