I compilatori di famiglie ML fanno qualche ottimizzazione sofisticata per le chiamate tail?

Question

I (credo) la seguente definizione di funzione è ricorsiva in coda:

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

Banalmente, è equivalente alla seguente dichiarazione

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

Eppure, in questa versione l'ultimo passo è quello di applicare la 'AndAlso ', quindi non è ricorsivo alla coda. O sembrerebbe di sì, tranne che dal momento che (almeno Standard) ML (di NJ) utilizza la valutazione di cortocircuito, l'andalso è in realtà/non/l'ultimo passo. Quindi questa funzione avrebbe un'ottimizzazione di coda? O ci sono altri casi interessanti in cui una funzione ML che ovviamente non usa la ricorsione in coda viene in effetti ottimizzata?

Answer 1

Se traduco la vostra seconda funzione di OCaml ottengo questo:

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

Questa è compilato come una funzione ricorsiva in coda per ocamlopt. L'essenza del codice generato (x86_64) è questo:

 .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 

Come potete vedere non ci sono chiamate ricorsive In questo codice, solo un ciclo.

(Ma altri manifesti sono giusto che OCaml non fa più di tanto in termini di analisi sofisticate. Questo particolare risultato sembra abbastanza semplice.)

Answer 2

Nota che

A andalso B 

è equivalente a

if A then B else false 

La definizione del linguaggio SML la definisce anche in questo modo. Di conseguenza, B è in posizione di coda. Non è necessaria alcuna ottimizzazione di fantasia.