ATS：使用定理证明/尾调用和尾递归进行编程

尾递归对于 ATS 中的编程至关重要。

假设一个函数 foo 调用一个函数 bar，其中 foo 和 bar 可以是同一个函数。如果对 bar 的调用返回值也是 foo 的返回值，那么此对 bar 的调用通常被称为尾调用。如果 foo 和 bar 是同一个函数，那么这就是一个（递归）自尾调用。例如，在如下定义的函数 f91 的主体中，有两个递归调用

fun f91 (n: int): int = if n >= 101 then n - 10 else f91 (f91 (n+11))

外部递归调用是自尾调用，而内部调用则不是。

如果一个函数主体中的每个递归调用都是尾调用，那么这个函数就是一个尾递归函数。例如，以下函数 sum2 是尾递归的

fun sum2 (n: int, res: int): int = if n > 0 then sum2 (n-1, n+res) else res

在 ATS 中，最重要的优化可能是将自尾调用转换为（局部）跳转的优化。这种优化实际上将每个尾递归函数转换为等效的循环。虽然 ATS 为构建 for 循环和 while 循环提供了直接的语法支持，但 ATS 中循环构建的首选方法是使用尾递归函数。