Lean函数定义

Lean函数定义

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

介绍

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

一个典型的Lean函数定义包含以下部分：

• 函数名称
• 参数列表（可选）
• 返回类型（可选，Lean支持类型推断）
• 函数体（实现逻辑）

基本语法

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

-- 定义一个函数，计算两个整数的和
def add (x : Int) (y : Int) : Int :=
  x + y

参数与类型标注

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

-- 显式类型标注
def multiply (x : Nat) (y : Nat) : Nat :=
  x * y

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

多参数与柯里化

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

-- 柯里化函数
def addThree (x : Nat) (y : Nat) (z : Nat) : Nat :=
  x + y + z

-- 部分应用
def addTwoToFive := addThree 2 5

函数应用与求值

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

#eval add 3 5  -- 输出: 8
#eval multiply 4 6  -- 输出: 24

模式匹配

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

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

#eval factorial 5  -- 输出: 120

高阶函数

高阶函数是指以函数为参数或返回函数的函数。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

实际案例

以下是一个实际案例，展示如何在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]

图表展示

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

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

数学公式

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

def f (x : Nat) := x^2

总结

Lean函数定义是函数式编程的基础，具有以下特点：

• 支持显式或隐式类型标注。
• 支持柯里化和高阶函数。
• 支持模式匹配和递归定义。
• 语法简洁，适合数学和算法实现。

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