编辑“︁Lean函数调用”︁

= Lean函数调用 =

'''Lean函数调用'''是Lean函数式编程中的基础概念之一，它描述了如何执行一个函数并获取其结果。在Lean中，函数调用遵循数学函数的定义方式，即通过传入参数（输入）来获得返回值（输出）。本文将详细介绍Lean函数调用的语法、规则、实际应用以及常见模式。

== 基本概念 ==

在Lean中，函数调用是通过将参数传递给函数来实现的。与其他编程语言（如Python或Java）不同，Lean的函数调用不需要使用括号来包裹参数列表，而是直接通过空格分隔函数名和参数。这种语法风格源自函数式编程的数学传统。

=== 语法结构 ===
函数调用的基本语法如下：
<syntaxhighlight lang="lean">
function_name argument1 argument2 ... argumentN
</syntaxhighlight>
其中：
* '''function_name''' 是函数名称。
* '''argument1''' 到 '''argumentN''' 是传递给函数的参数。

=== 示例：简单函数调用 ===
以下是一个简单的函数定义和调用示例：
<syntaxhighlight lang="lean">
def add (x : Nat) (y : Nat) : Nat := x + y

#eval add 2 3  -- 输出: 5
</syntaxhighlight>
在这个例子中：
1. '''add''' 是一个接收两个自然数（'''Nat'''）并返回它们的和的函数。
2. '''add 2 3''' 是函数调用，传入参数2和3，返回5。

== 函数调用的特性 ==

=== 柯里化（Currying） ===
Lean中的函数是'''柯里化'''的，这意味着多参数函数可以被分解为一系列单参数函数的嵌套调用。例如：
<syntaxhighlight lang="lean">
def multiply (x : Nat) (y : Nat) : Nat := x * y

-- 柯里化调用
#eval multiply 2 3  -- 输出: 6
#eval (multiply 2) 3  -- 等价于上一行，输出: 6
</syntaxhighlight>
这里，'''multiply 2''' 返回一个函数，该函数接收一个参数 '''y''' 并返回 '''2 * y'''。

=== 部分应用 ===
由于柯里化的特性，Lean允许'''部分应用'''函数，即只提供部分参数：
<syntaxhighlight lang="lean">
def double := multiply 2  -- 部分应用 multiply，固定第一个参数为2

#eval double 5  -- 输出: 10
</syntaxhighlight>

=== 高阶函数调用 ===
Lean支持高阶函数，即函数可以作为参数或返回值传递。例如：
<syntaxhighlight lang="lean">
def applyTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x)

#eval applyTwice (fun x => x + 1) 2  -- 输出: 4
</syntaxhighlight>
这里，'''applyTwice''' 接收一个函数 '''f''' 和一个值 '''x'''，并调用 '''f''' 两次。

== 实际应用案例 ==

=== 递归函数调用 ===
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 length {α : Type} (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | _ :: ys => 1 + length ys

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

== 函数调用的可视化 ==
以下是一个函数调用过程的示意图：
<mermaid>
graph LR
    A[调用函数 add 2 3] --> B[计算 2 + 3]
    B --> C[返回结果 5]
</mermaid>

== 数学公式表示 ==
函数调用可以表示为数学映射：
<math>f : A \rightarrow B</math>，其中：
* <math>A</math> 是输入类型。
* <math>B</math> 是输出类型。
例如，'''add''' 可以表示为：
<math>\text{add} : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}</math>

== 总结 ==
Lean的函数调用是函数式编程的核心机制之一，其特点包括：
* 简洁的语法（无需括号）。
* 柯里化和部分应用支持。
* 高阶函数能力。
* 递归和依赖类型的强大表达力。

通过掌握这些概念，你可以更高效地编写Lean程序，并利用其类型系统的优势构建可靠的软件。

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