尾递归

虽然 Lean 的 do-记法允许使用传统的循环语法，例如 for 和 while，但这些结构在幕后会被翻译为递归函数的调用。在大多数编程语言中，递归函数相对于循环有一个关键缺点：循环不消耗堆栈空间，而递归函数消耗与递归调用次数成正比的栈空间。栈空间通常是有限的，通常有必要将以递归函数自然表达的算法，重写为用显式可变堆来分配栈的循环。

在函数式编程中，情况通常相反。以可变循环自然表达的程序可能会消耗栈空间，而将它们重写为递归函数可以使它们快速运行。这是函数式编程语言的一个关键方面： 尾调用消除（Tail-call Elimination）。尾调用是从一个函数到另一个函数的调用，可以编译成一个普通的跳转，替换当前的栈帧而非压入一个新的栈帧，而尾调用消除就是实现此转换的过程。

尾调用消除不仅仅是一种可选的优化。它的存在是编写高效函数式代码的基础部分。为了使其有效，它必须是可靠的。程序员必须能够可靠地识别尾调用，并且他们必须相信编译器会消除它们。

函数 NonTail.sum 将 Nat 列表的内容加起来:

def NonTail.sum : List Nat → Nat
  | [] => 0
  | x :: xs => x + sum xs

将此函数应用于列表 [1, 2, 3] 会产生以下求值步骤：

NonTail.sum [1, 2, 3]
===>
1 + (NonTail.sum [2, 3])
===>
1 + (2 + (NonTail.sum [3]))
===>
1 + (2 + (3 + (NonTail.sum [])))
===>
1 + (2 + (3 + 0))
===>
1 + (2 + 3)
===>
1 + 5
===>
6

在求值步骤中，括号表示对 NonTail.sum 的递归调用。换句话说，要加起来这三个数字，程序必须首先检查列表是否非空。要将列表的头部（1）加到列表尾部的和上，首先需要计算列表尾部的和：

1 + (NonTail.sum [2, 3])

但是要计算列表尾部的和，程序必须检查它是否为空，然而它不是。尾部本身是一个列表，头部为 2。结果步骤正在等待 NonTail.sum [3] 的返回：

1 + (2 + (NonTail.sum [3]))

运行时调用栈的重点在于跟踪值 1、2 和 3，以及一个指令将它们加到递归调用的结果上。随着递归调用的完成，控制权返回到发出调用的栈帧，于是每一步的加法都被执行了。存储列表的头部和将它们相加的指令并不是免费的；它占用的空间与列表的长度成正比。

函数 Tail.sum 也将 Nat 列表的内容加起来：

def Tail.sumHelper (soFar : Nat) : List Nat → Nat
  | [] => soFar
  | x :: xs => sumHelper (x + soFar) xs

def Tail.sum (xs : List Nat) : Nat :=
  Tail.sumHelper 0 xs

将其应用于列表 [1, 2, 3] 会产生以下求值步骤：

Tail.sum [1, 2, 3]
===>
Tail.sumHelper 0 [1, 2, 3]
===>
Tail.sumHelper (0 + 1) [2, 3]
===>
Tail.sumHelper 1 [2, 3]
===>
Tail.sumHelper (1 + 2) [3]
===>
Tail.sumHelper 3 [3]
===>
Tail.sumHelper (3 + 3) []
===>
Tail.sumHelper 6 []
===>
6

The internal helper function calls itself recursively, but it does so in a way where nothing needs to be remembered in order to compute the final result. When Tail.sumHelper reaches its base case, control can be returned directly to Tail.sum, because the intermediate invocations of Tail.sumHelper simply return the results of their recursive calls unmodified. In other words, a single stack frame can be re-used for each recursive invocation of Tail.sumHelper. Tail-call elimination is exactly this re-use of the stack frame, and Tail.sumHelper is referred to as a tail-recursive function. 内部的辅助函数以递归方式调用自身，但它以一种新的方式执行此操作，无需记住任何内容即可计算最终结果。当 Tail.sumHelper 达到其基本情况时，控制权可以直接返回到 Tail.sum，因为 Tail.sumHelper 的中间调用只是返回其递归调用的结果，而不会修改结果。换句话说，可以为 Tail.sumHelper 的每个递归调用重新使用一个栈帧。尾调用消除正是这种栈帧的重新使用，而 Tail.sumHelper 被称为 尾递归函数（Tail-Recursive Function）。

Tail.sumHelper 的第一个参数包含所有其他需要在调用栈中跟踪的信息，即到目前为止遇到的数字的总和。在每个递归调用中，此参数都会使用新信息进行更新，而非将新信息添加到调用栈中。替换调用栈中信息的 soFar 等参数称为 累加器（Accumulator）。

在撰写本文时，在作者的计算机上，当传入包含 216,856 个或更多条目的列表时， NonTail.sum 会因栈溢出而崩溃。另一方面，Tail.sum 可以对包含 100,000,000 个元素的列表求和，而不会发生栈溢出。由于在运行 Tail.sum 时不需要压入新的栈帧，因此它完全等同于一个 while 循环，其中一个可变变量保存当前列表。在每次递归调用中，栈上的函数参数都会被简单地替换为列表的下一个节点。

尾部与非尾部位置

Tail.sumHelper 是尾递归的原因在于递归调用处于 尾部位置。非正式地说，当调用者不需要以任何方式修改返回值，而是会直接返回它时，函数调用就处于尾部位置。更正式地说，尾部位置可以显式地为表达式定义。

如果 match-表达式处于尾部位置，那么它的每个分支也处于尾部位置。一旦 match 选择了一个分支，控制权就会立即传递给它。与此类似，如果 if 表达式本身处于尾部位置，那么 if 表达式的两个分支都处于尾部位置。最后，如果 let 表达式处于尾部位置，那么它的主体也是如此。

所有其他位置都不处于尾部位置。函数或构造子的参数不处于尾部位置，因为求值必须跟踪会应用到参数值的函数或构造子。内部函数的主体不处于尾部位置，因为控制权甚至可能不会传递给它：函数主体在函数被调用之前不会被求值。与此类似，函数类型的函数主体不处于尾部位置。要求值 (x : α) → E 中的 E，就有必要跟踪结果，结果的类型必须有 (x : α) → ... 包裹在其周围。

在 NonTail.sum 中，递归调用不在尾部位置，因为它是一个 + 的参数。在 Tail.sumHelper 中，递归调用在尾部位置，因为它紧跟在模式匹配之后，而模式匹配本身是函数的主体。

在撰写本文时，Lean 仅消除了递归函数中的直接尾部调用。这意味着在 f 的定义中对 f 的尾部调用将被消除，但对其他函数 g 的尾部调用不会被消除。当然，消除其他函数的尾部调用以节省栈帧是可行的，但这尚未在 Lean 中实现。

反转列表

函数 NonTail.reverse 通过将每个子列表的头部追加到结果的末尾来反转列表：

def NonTail.reverse : List α → List α
  | [] => []
  | x :: xs => reverse xs ++ [x]

使用它来反转 [1, 2, 3] 会产生以下步骤：

NonTail.reverse [1, 2, 3]
===>
(NonTail.reverse [2, 3]) ++ [1]
===>
((NonTail.reverse [3]) ++ [2]) ++ [1]
===>
(((NonTail.reverse []) ++ [3]) ++ [2]) ++ [1]
===>
(([] ++ [3]) ++ [2]) ++ [1]
===>
([3] ++ [2]) ++ [1]
===>
[3, 2] ++ [1]
===>
[3, 2, 1]

尾递归版本会在每一步的累加器上使用 x :: · 而非 · ++ [x]：

def Tail.reverseHelper (soFar : List α) : List α → List α
  | [] => soFar
  | x :: xs => reverseHelper (x :: soFar) xs

def Tail.reverse (xs : List α) : List α :=
  Tail.reverseHelper [] xs

这是因为在使用 NonTail.reverse 计算时保存在每个栈帧中的上下文从基本情况开始应用。每个「记住的」上下文片段都按照后进先出的顺序执行。另一方面，累加器传递版本从列表中的第一个条目而非原始基本情况开始修改累加器，如以下归约步骤所示：

Tail.reverse [1, 2, 3]
===>
Tail.reverseHelper [] [1, 2, 3]
===>
Tail.reverseHelper [1] [2, 3]
===>
Tail.reverseHelper [2, 1] [3]
===>
Tail.reverseHelper [3, 2, 1] []
===>
[3, 2, 1]

换句话说，非尾递归版本从基本情况开始，从右到左通过列表修改递归结果。列表中的条目以先入先出的顺序影响累加器。带有累加器的尾递归版本从列表的头部开始，从左到右通过列表修改初始累加器值。

由于加法满足交换律，因此无需在 Tail.sum 中对此进行处理。列表追加不满足交换律，因此必须注意要找到一个在相反方向运行时具有相同效果的操作。在 NonTail.reverse 中，在递归结果后追加 [x] 与以逆序构建结果时将 x 添加到列表开头类似。

多个递归调用

在 BinTree.mirror 的定义中，有两个递归调用：

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

就像命令式语言通常会对 reverse 和 sum 等函数使用 while 循环一样，它们通常会对这种遍历使用递归函数。此函数无法直接通过累加器传递风格重写为尾递归函数。

通常，如果每个递归步骤需要多个递归调用，那么将很难使用累加器传递样式。这种困难类似于使用循环和显式数据结构重写递归函数的困难，增加了说服 Lean 函数终止的复杂性。但是，就像在 BinTree.mirror 中一样，多个递归调用通常表示一个数据结构，其构造子具有多次递归出现的情况。在这些情况下，结构的深度通常与其整体大小成对数关系，这使得栈和堆之间的权衡不那么明显。有一些系统化的技术可以使这些函数成为尾递归，例如使用 续体传递风格（Continuation-Passing Style），但它们超出了本章的范围。

练习

将以下所有非尾递归的函数翻译成累加器传递的尾递归函数：

def NonTail.length : List α → Nat
  | [] => 0
  | _ :: xs => NonTail.length xs + 1

def NonTail.factorial : Nat → Nat
  | 0 => 1
  | n + 1 => factorial n * (n + 1)

NonTail.filter 的翻译应当产生一个程序，它通过尾递归占用常量栈空间，运行时间与输入列表的长度成线性相关。相对于原始情况来说，常数因子的开销是可以接受的：

def NonTail.filter (p : α → Bool) : List α → List α
  | [] => []
  | x :: xs =>
    if p x then
      x :: filter p xs
    else
      filter p xs

Lean 函数式编程

尾递归

尾部与非尾部位置

反转列表

多个递归调用

练习