编辑“︁Lean函数定义”︁

= Lean函数定义 =

'''Lean函数定义'''是Lean函数式编程中最基础且核心的概念之一。它描述了如何在Lean中声明和实现函数，包括函数的输入参数、输出类型以及函数体逻辑。在Lean中，函数是“一等公民”，这意味着它们可以像其他值一样被传递、返回和操作。

== 介绍 ==

在Lean中，函数定义遵循函数式编程范式，强调不可变性和纯函数（即相同的输入总是产生相同的输出，且不产生副作用）。Lean的函数定义语法简洁且富有表现力，支持类型推断、模式匹配和高阶函数等特性。

一个典型的Lean函数定义包含以下部分：
* 函数名称
* 参数列表（可选）
* 返回类型（可选，Lean支持类型推断）
* 函数体（实现逻辑）

== 基本语法 ==

Lean的函数定义通常以`def`关键字开头，后跟函数名称、参数列表、返回类型（用冒号`:`指定）和函数体。以下是一个简单的例子：

<syntaxhighlight lang="lean">
-- 定义一个函数，计算两个整数的和
def add (x : Int) (y : Int) : Int :=
  x + y
</syntaxhighlight>

=== 参数与类型标注 ===
Lean支持显式类型标注，但也可以利用类型推断自动推导类型。例如：

<syntaxhighlight lang="lean">
-- 显式类型标注
def multiply (x : Nat) (y : Nat) : Nat :=
  x * y

-- 类型推断（Lean会自动推导`x`和`y`的类型为`Nat`）
def square (x) :=
  x * x
</syntaxhighlight>

=== 多参数与柯里化 ===
Lean中的函数是“柯里化”的，即多参数函数可以分解为一系列单参数函数。例如：

<syntaxhighlight lang="lean">
-- 柯里化函数
def addThree (x : Nat) (y : Nat) (z : Nat) : Nat :=
  x + y + z

-- 部分应用
def addTwoToFive := addThree 2 5
</syntaxhighlight>

== 函数应用与求值 ==

Lean中的函数通过“应用”来调用。函数应用的语法是简单的空格分隔，例如：

<syntaxhighlight lang="lean">
#eval add 3 5  -- 输出: 8
#eval multiply 4 6  -- 输出: 24
</syntaxhighlight>

== 模式匹配 ==

Lean支持基于模式匹配的函数定义，这是一种强大的特性，允许根据输入的结构来定义函数行为。例如：

<syntaxhighlight lang="lean">
-- 定义一个递归函数计算阶乘
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 5  -- 输出: 120
</syntaxhighlight>

== 高阶函数 ==

高阶函数是指以函数为参数或返回函数的函数。Lean中高阶函数的定义示例如下：

<syntaxhighlight lang="lean">
-- 接受一个函数作为参数
def applyTwice (f : Nat → Nat) (x : Nat) : Nat :=
  f (f x)

-- 返回一个函数
def makeAdder (n : Nat) : Nat → Nat :=
  fun x => x + n

#eval applyTwice (fun x => x * 2) 3  -- 输出: 12
#eval makeAdder 5 10  -- 输出: 15
</syntaxhighlight>

== 实际案例 ==

以下是一个实际案例，展示如何在Lean中定义一个函数来过滤列表中的偶数：

<syntaxhighlight lang="lean">
-- 定义一个函数过滤列表中的偶数
def filterEven : List Nat → List Nat
  | [] => []
  | x :: xs =>
    if x % 2 == 0 then
      x :: filterEven xs
    else
      filterEven xs

#eval filterEven [1, 2, 3, 4, 5]  -- 输出: [2, 4]
</syntaxhighlight>

== 图表展示 ==

以下是一个函数调用流程的Mermaid图：

<mermaid>
graph TD
  A[调用 add 3 5] --> B[计算 3 + 5]
  B --> C[返回 8]
</mermaid>

== 数学公式 ==

Lean函数定义可以用数学公式表示。例如，函数<math>f(x) = x^2</math>在Lean中定义为：

<syntaxhighlight lang="lean">
def f (x : Nat) := x^2
</syntaxhighlight>

== 总结 ==

Lean函数定义是函数式编程的基础，具有以下特点：
* 支持显式或隐式类型标注。
* 支持柯里化和高阶函数。
* 支持模式匹配和递归定义。
* 语法简洁，适合数学和算法实现。

通过掌握Lean函数定义，你可以构建复杂的函数式程序，并利用Lean强大的类型系统和定理证明能力。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean函数式编程]]