Lean 函数定义
在Lean中，函数是编程的核心构建块之一。函数式编程强调使用纯函数来构建程序，而Lean作为一门函数式编程语言，提供了简洁而强大的函数定义方式。本文将带你从基础开始，逐步掌握Lean中的函数定义。
什么是函数？
在编程中，函数是一段可重用的代码块，它接受输入（称为参数），并返回输出（称为返回值）。在Lean中，函数是“一等公民”，这意味着函数可以像其他值一样被传递、存储和操作。
基础函数定义
在Lean中，定义一个函数的基本语法如下：
def 函数名 (参数1 : 类型1) (参数2 : 类型2) : 返回类型 :=
函数体
让我们从一个简单的例子开始：
def add (x : Nat) (y : Nat) : Nat :=
x + y
在这个例子中，我们定义了一个名为 add 的函数，它接受两个自然数（Nat）作为参数，并返回它们的和。
调用函数
定义函数后，我们可以通过传递参数来调用它：
#eval add 2 3 -- 输出: 5
#eval 是Lean中的一个命令，用于计算表达式的值并输出结果。
多参数与柯里化
Lean中的函数支持多参数，并且默认情况下是柯里化的。这意味着你可以部分应用函数，即只传递部分参数，返回一个新的函数。
def multiply (x : Nat) (y : Nat) : Nat :=
x * y
def double : Nat → Nat :=
multiply 2
#eval double 5 -- 输出: 10
在这个例子中，multiply 函数接受两个参数，而 double 是 multiply 的部分应用，只传递了一个参数 2，返回了一个新的函数。
递归函数
Lean支持递归函数，即函数可以在其定义中调用自身。递归是函数式编程中处理循环和迭代的常见方式。
def factorial : Nat → Nat
| 0 => 1
| n + 1 => (n + 1) * factorial n
#eval factorial 5 -- 输出: 120
在这个例子中，factorial 函数通过模式匹配来处理递归。当输入为 0 时，返回 1；否则，递归调用 factorial 并乘以当前值。
在定义递归函数时，确保递归调用最终会终止，否则可能导致无限循环。
高阶函数
高阶函数是指接受其他函数作为参数或返回函数的函数。Lean中的高阶函数使得代码更加灵活和模块化。
def applyTwice (f : Nat → Nat) (x : Nat) : Nat :=
f (f x)
#eval applyTwice double 3 -- 输出: 12
在这个例子中，applyTwice 是一个高阶函数，它接受一个函数 f 和一个值 x，并将 f 应用两次到 x 上。
实际应用场景
列表映射
在函数式编程中，列表操作是非常常见的。Lean提供了丰富的列表操作函数，例如 map，它可以将一个函数应用到列表的每个元素上。
def square (x : Nat) : Nat :=
x * x
#eval List.map square [1, 2, 3, 4] -- 输出: [1, 4, 9, 16]
在这个例子中，List.map 将 square 函数应用到列表 [1, 2, 3, 4] 的每个元素上，返回一个新的列表。
过滤器
另一个常见的列表操作是 filter，它可以根据条件过滤列表中的元素。
def isEven (x : Nat) : Bool :=
x % 2 == 0
#eval List.filter isEven [1, 2, 3, 4, 5, 6] -- 输出: [2, 4, 6]
在这个例子中，List.filter 使用 isEven 函数过滤出列表中的偶数。
总结
在本文中，我们介绍了Lean中函数定义的基础知识，包括简单函数、递归函数、高阶函数以及它们在列表操作中的应用。函数式编程的核心在于使用纯函数来构建程序，而Lean提供了强大的工具来支持这一范式。
为了巩固你的知识，尝试定义一些自己的函数，例如计算斐波那契数列或实现列表的折叠操作。
附加资源
- Lean官方文档
- 《函数式编程思维》—— Michael Fogus
- 《Lean编程入门》—— Jeremy Avigad
通过不断练习和探索，你将能够熟练地使用Lean中的函数定义，并构建出高效、模块化的程序。