Lean函数类型

Lean函数类型是Lean定理证明器类型系统的核心组成部分，它表示输入类型到输出类型的映射关系。函数类型在Lean中不仅是编程的基础构造，也是数学命题和证明的载体。本文将详细解释其语法、行为及实际应用。

基本概念

在Lean中，函数类型写作 α → β（或 ∀ (x : α), β），表示从类型 α 到类型 β 的映射。若 β 依赖输入值 x : α，则使用Π类型（Π (x : α), β x），但在非依赖情况下与箭头类型等价。

语法示例

  
-- 非依赖函数类型  
def double : Nat → Nat := fun x => x * 2  

-- 依赖函数类型（Π类型）  
def repeat : Π (n : Nat) (s : String), String :=  
  fun n s => String.append s (String.replicate (n - 1) s)

求值行为

函数调用通过传递参数实现：

  
#eval double 3  -- 输出: 6  
#eval repeat 2 "hi"  -- 输出: "hihi"

高阶函数

Lean支持将函数作为参数或返回值。例如：

  
def applyTwice : (Nat → Nat) → Nat → Nat :=  
  fun f x => f (f x)  

#eval applyTwice double 2  -- 输出: 8（2 → 4 → 8）

柯里化与部分应用

Lean函数默认柯里化，可部分应用：

  
def add : Nat → Nat → Nat := fun x y => x + y  
def addFive := add 5  -- 类型: Nat → Nat  

#eval addFive 3  -- 输出: 8

函数与命题

在命题即类型（Curry-Howard对应）下，函数类型对应逻辑蕴含：

• α → β 表示“若α成立，则β成立”。
• 函数实现即为蕴含的证明。

示例证明

  
example : ∀ (P Q : Prop), P → (Q → P) :=  
  fun P Q p q => p  -- 构造一个忽略Q的常量函数

实际应用案例

列表映射

使用函数类型处理列表：

  
def mapList : (α → β) → List α → List β  
  | _, [] => []  
  | f, h :: t => f h :: mapList f t  

#eval mapList double [1, 2, 3]  -- 输出: [2, 4, 6]

依赖函数与定理

依赖类型允许精确约束：

  
-- 定义长度索引向量  
inductive Vec (α : Type) : Nat → Type  
  | nil : Vec α 0  
  | cons : α → Vec α n → Vec α (n + 1)  

-- 确保返回向量长度与输入相同  
def mapVec : (α → β) → Vec α n → Vec β n  
  | _, Vec.nil => Vec.nil  
  | f, Vec.cons x xs => Vec.cons (f x) (mapVec f xs)

可视化：函数类型关系

graph LR A[α] -->|输入| B[函数 f : α → β] B -->|输出| C[β]

数学表示

函数类型可形式化为： $f:\alpha \to \beta \text{或}\prod _{x:\alpha }\beta (x)$

总结

• Lean函数类型是**一等公民**，支持高阶操作。
• 箭头类型与Π类型统一处理非依赖/依赖场景。
• 柯里化简化部分应用，便于组合。
• 在命题证明中，函数对应逻辑蕴含的构造过程。

通过本文的代码示例和理论解释，读者应能掌握Lean函数类型的核心机制及其在编程与证明中的双重作用。