ML家族编译器是否对尾调用进行任何复杂的优化？

Question

我(相信)以下函数定义是尾递归的:

fun is_sorted [] = true
  | is_sorted [x] = true
  | is_sorted (x::(y::xs)) =
    if x > y
       then false
       else is_sorted (y::xs)

琐碎的是,它等同于以下声明

fun is_sorted [] = true
  | is_sorted [x] = true
  | is_sorted (x::(y::xs)) = 
    (x <= y) andalso (is_sorted (y::xs))

然而在这个版本中,最后一步是应用'andalso',所以它不是尾递归的.或者它似乎是这样,除了因为(至少是标准的)ML(NJ)使用短路评估,并且实际上/不是/最后一步.那么这个函数会有尾调用优化吗？还是有任何其他有趣的实例,其中明显使用尾递归的ML函数实际上得到优化？

Answer 1

注意

A andalso B

相当于

if A then B else false

SML语言定义甚至以这种方式定义它.因此,B 是在尾部位置.不需要花哨的优化.

Answer 2

如果我将你的第二个函数翻译成 OCaml，我会得到这个：

let rec is_sorted : int list -> bool = function
| [] -> true
| [_] -> true
| x :: y :: xs -> x < y && is_sorted xs

这被 ocamlopt 编译为尾递归函数。生成的代码（x86_64）的本质是这样的：

        .globl      _camlAndalso__is_sorted_1008
_camlAndalso__is_sorted_1008:
        .cfi_startproc
.L103:
        cmpq        $1, %rax
        je  .L100
        movq        8(%rax), %rbx
        cmpq        $1, %rbx
        je  .L101
        movq        (%rbx), %rdi
        movq        (%rax), %rax
        cmpq        %rdi, %rax
        jge .L102
        movq        8(%rbx), %rax
        jmp .L103
        .align      2
.L102:
        movq        $1, %rax
        ret
        .align      2
.L101:
        movq        $3, %rax
        ret
        .align      2
.L100:
        movq        $3, %rax
        ret
        .cfi_endproc

如您所见，此代码中没有递归调用，只有一个循环。

（但其他海报是正确的，OCaml 在复杂分析方面并没有做那么多。这个特殊的结果似乎很简单。）