Is my rec function tail recursive?

Question

Is this function tail-recursive ?

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)

In general, is there a way to formally check it ?

Thanks.

Answer 1

This function is tail-recursive; I can tell by eyeballing it.

In general it is not always easy to tell. Perhaps the most reliable/pragmatic thing is just to check it on a large input (and make sure you are compiling in 'Release' mode, as 'Debug' mode turns off tail calls for better debugging).

Answer 2

Yes, you can formally prove that a function is tail-recursive. Every expression reduction has a tail-position, and if all recursions are in tail-positions then the function is tail-recursive. It's possible for a function to be tail-recursive in one place, but not in another.

In the expression let pat = exprA in exprB only exprB is in tail-position. That is, while you can go evaluate exprA, you still have to come back to evaluate exprB with exprA in mind. For every expression in the language, there's a reduction rule that tells you where the tail position is. In ExprA; ExprB it's ExprB again. In if ExprA then ExprB else ExprC it's both ExprB and ExprC and so on.

The compiler of course knows this as it goes. However the many expressions available in F# and the many internal optimizations carried out by the compiler as it goes, e.g. during pattern match compiling, computation expressions like seq{} or async{} can make knowing which expressions are in tail-position non-obvious.

Practically speaking, with some practice it's easy for small functions to determine a tail call by just looking at your nested expressions and checking the slots which are NOT in tail positions for function calls. (Remember that a tail call may be to another function!)