我的rec函数是尾递归的吗？

Question

这个函数是尾递归的吗？

let rec rec_algo1 step J = 
    if step = dSs then J
    else
        let a = Array.init (Array2D.length1 M) (fun i -> minby1J i M J)
        let argmin = a|> Array.minBy snd |> fst
        rec_algo1 (step+1) (argmin::J)

一般来说，有没有办法正式检查它？

谢谢。

Answer 1

该函数是尾递归的；我用肉眼就能看出来。

一般来说，这并不总是容易判断。也许最可靠/务实的事情就是在大输入上检查它（并确保您在“发布”模式下进行编译，因为“调试”模式会关闭尾部调用以实现更好的调试）。

Answer 2

是的，您可以正式证明函数是尾递归的。每个表达式归约都有一个尾位置，如果所有递归都位于尾位置，则该函数是尾递归的。函数有可能在一个地方是尾递归的，但在另一个地方却不是。

在表达式 let pat = exprA in exprB 中，只有 exprB 位于尾部位置。也就是说，虽然您可以去评估 exprA，但您仍然必须回来评估 exprB 并牢记 exprA。对于该语言中的每个表达式，都有一个归约规则告诉您尾部位置在哪里。在ExprA中； ExprB 又是ExprB。在 if ExprA then ExprB else ExprC 中，它既是 ExprB 又是 ExprC 等等。

编译器当然知道这一点。然而，F# 中提供了许多可用的表达式，以及编译器在运行过程中执行的许多内部优化，例如在模式匹配编译期间、seq{} 或 async{} 等计算表达式> 可以使知道哪些表达式位于尾部位置变得不明显。

实际上，通过一些实践，小函数很容易通过查看嵌套表达式并检查不在函数调用尾部位置的槽来确定尾部调用。 （请记住，尾部调用可能是另一个函数！）

Answer 3

你问我们如何正式检查这一点，以便我尝试一下。我们首先必须定义函数尾递归的含义。 该形式的递归函数定义

let rec f x_1 ... x_n = e

如果 e 内对 f 的所有调用都是尾调用，则 是尾递归的 - 即。发生在尾部上下文中。 尾部上下文 C 被归纳地定义为带有空洞 [] 的术语：

C ::= []
    | e
    | let p = e in C
    | e; C
    | match e with p_1 -> C | ... | p_n -> C
    | if e then C else C

其中 e 是 F# 表达式，x 是一个变量，p 是一个模式。我们应该将其扩展为相互递归函数定义，但我将其作为练习。

现在让我们将其应用到您的示例中。函数体中对 rec_algo1 的唯一调用是在此上下文中：

if step = dSs then J
else
    let a = Array.init (Array2D.length1 M) (fun i -> minby1J i M J)
    let argmin = a|> Array.minBy snd |> fst
    []

并且由于这是尾上下文，因此该函数是尾递归的。这就是函数式程序员观察它的方式 - 扫描定义的主体以查找递归调用，然后验证每个调用是否出现在尾部上下文中。尾部调用的一个更直观的定义是，除了返回调用结果之外，没有对调用结果执行任何其他操作。