# 函数
> lambda 与 fun、三种参数绑定（显式/隐式/实例）、命名参数与默认值、递归与终止性。
- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/functions
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）
## 定义方式
```lean
-- 1. def
def double (n : Nat) : Nat := n * 2
-- 2. lambda（匿名函数）
def double' : Nat → Nat := fun n => n * 2
-- 3. λ 是 fun 的同义词
def double'' : Nat → Nat := λ n => n * 2
```
**Lean 4 用 `=>`，不是 Lean 3 的逗号。**
```lean
fun n => n * 2 -- ✅ Lean 4
-- λ n, n * 2 -- ❌ Lean 3 语法，报错
```
这是从 Lean 3 教程迁移时最先撞上的差异。
多参数 lambda：
```lean
#check fun (a b : Nat) => a + b -- Nat → Nat → Nat
#eval (fun a b => a + b) 3 4 -- 7
```
## 三种参数绑定
这是 Lean 与多数语言最不同的地方之一。
| 括号 | 名称 | 调用时 |
| --- | --- | --- |
| `(x : α)` | **显式** | 必须给 |
| `{x : α}` | **隐式** | 由 Lean 从其他参数推断 |
| `[Inst α]` | **实例隐式** | 由类型类推断求解 |
| `⦃x : α⦄` | 严格隐式 | 仅当后面还有显式参数时才推断 |
### 隐式参数
```lean
def myId {α : Type} (a : α) : α := a
#eval myId 42 -- 不用写 α，Lean 从 42 推断出 Nat
#eval myId "hi"
```
如果 `α` 是显式的，每次调用都要写 `myId Nat 42`——极其啰嗦。**类型参数几乎总是隐式的**。
需要显式指定时，用 `@` 关闭所有隐式：
```lean
#check @myId -- {α : Type} → α → α
#eval @myId Nat 42 -- 42
```
或用命名参数只指定某一个：
```lean
#eval myId (α := Nat) 42
```
**`@` 是排查类型问题的利器。** 当 Lean 推断出你不期望的隐式参数时，`@f` 能看到完整签名，`#check @f` 常常一眼看出问题。
### 实例隐式
```lean
def sum3 [Add α] (a b c : α) : α := a + b + c
```
`[Add α]` 表示「需要 `α` 上的加法实例，由类型类系统去找」。详见[类型类](https://daiw.org/manual/lean4/typeclasses)。
## 命名参数与默认值
```lean
def greet (name : String) (greeting : String := "Hello") : String :=
s!"{greeting}, {name}!"
#eval greet "Lean" -- "Hello, Lean!"
#eval greet "Lean" "Hi" -- "Hi, Lean!"
#eval greet (name := "Lean") (greeting := "Hey")
```
`:=` 在参数位置表示**默认值**。命名参数还允许乱序传参。
另有自动填充的参数：
```lean
def f (n : Nat) (h : n > 0 := by decide) : Nat := n
```
`:= by tactic` 表示「这个参数由该 tactic 自动构造」——常用于自动满足的证明义务。
## 模式匹配
```lean
def isZero : Nat → Bool
| 0 => true
| _ + 1 => false
```
**方程式风格**：直接对参数分情况，不写 `fun`。这是 Lean 里最常用的函数定义方式。
`match` 表达式形式：
```lean
def isZero' (n : Nat) : Bool :=
match n with
| 0 => true
| _ + 1 => false
```
多参数同时匹配：
```lean
def bothZero : Nat → Nat → Bool
| 0, 0 => true
| _, _ => false
```
匹配是**穷尽性检查**的——漏掉情况会报错：
```lean
def bad : Nat → Bool
| 0 => true
-- error: missing cases: (Nat.succ _)
```
这是 Lean 相对多数语言的重要保障：**不可能有「忘记处理某个 case」的 bug**。
## 递归与终止性
```lean
def factorial : Nat → Nat
| 0 => 1
| n + 1 => (n + 1) * factorial n
```
Lean **必须确信递归会终止**——否则可以构造出任意命题的「证明」，系统就不一致了。
结构递归（参数严格变小）会被自动接受。复杂情况需要帮忙：
### termination_by
```lean
def gcd' (a b : Nat) : Nat :=
if h : b = 0 then a
else gcd' b (a % b)
termination_by b
decreasing_by
simp_wf
exact Nat.mod_lt _ (Nat.pos_of_ne_zero h)
```
- **`termination_by`** 指出「哪个量在变小」。
- **`decreasing_by`** 提供「它确实在变小」的证明。
**写不出终止性证明时，先怀疑函数本身。** 大多数情况下是递归结构确实有问题，而不是 Lean 太笨。
实在需要非终止函数（如解释器主循环），用 `partial def`：
```lean
partial def loop (n : Nat) : Nat := loop (n + 1)
```
代价是**该函数不能用于证明**——Lean 不会展开它的定义，只把它当一个不透明的黑箱。写程序可以，写数学不行。
## 结构化递归的辅助
```lean
def fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fib n + fib (n + 1)
```
多步的结构递归 Lean 也能自动处理。
要注意**这个朴素实现是指数复杂度**——`#eval fib 40` 会跑很久。高效版本用累加器：
```lean
def fibFast (n : Nat) : Nat :=
go n 0 1
where
go : Nat → Nat → Nat → Nat
| 0, a, _ => a
| n + 1, a, b => go n b (a + b)
```
`where` 定义局部辅助函数——比在顶层污染命名空间干净。
也可以用 `let rec`：
```lean
def fibFast' (n : Nat) : Nat :=
let rec go : Nat → Nat → Nat → Nat
| 0, a, _ => a
| n + 1, a, b => go n b (a + b)
go n 0 1
```
## 函数组合与管道
```lean
def addOne (n : Nat) : Nat := n + 1
def timesTwo (n : Nat) : Nat := n * 2
#eval (addOne ∘ timesTwo) 5 -- 11 先 ×2 再 +1
#eval (5 |> timesTwo |> addOne) -- 11 管道，从左往右读
#eval addOne <| timesTwo 5 -- 11 <| 相当于省括号
```
| 记号 | 输入 | 含义 |
| --- | --- | --- |
| `∘` | `\comp` | 函数组合，**右边先执行** |
| `\|>` | 直接打 | 管道，左边的值送进右边的函数 |
| `<\|` | 直接打 | 反向应用，避免写括号 |
`<|` 特别有用——它让 `f (g (h x))` 可以写成 `f <| g <| h x`。
## 匿名构造子与投影
```lean
structure Point where
x : Nat
y : Nat
def p : Point := ⟨1, 2⟩ -- 匿名构造子，⟨⟩ 是 \< \>
#eval p.x -- 1，点记法投影
#eval p.1 -- 1，位置投影
```
`.` 记法有个强大的用法叫**广义字段记法**：
```lean
def l : List Nat := [1, 2, 3]
#eval l.length -- 等价于 List.length l
#eval l.map (· * 2) -- 等价于 List.map (· * 2) l
```
**`x.f a` 会被解释成 `T.f x a`**（`T` 是 `x` 的类型）。这让代码读起来像面向对象，实际是纯函数调用。
## 中心点记法
```lean
#eval [1, 2, 3].map (· * 2) -- [2, 4, 6]
#eval [1, 2, 3].filter (· > 1) -- [2, 3]
```
`·`（`\.`）是**占位符**，`(· * 2)` 等价于 `fun x => x * 2`。作用域是**最近的括号**：
```lean
(· + ·) -- fun a b => a + b
(f · x) -- fun a => f a x
```
写短 lambda 时非常简洁，是 Lean 代码里的常见风格。
下一篇：[归纳类型与结构体](https://daiw.org/manual/lean4/inductive-types)。