3


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.

jliettehk
  • 33
  • 2
  • You can propably check if the compiler recognized it as such (after all, that's all that matters), but not without asking the compiler's for the results of the corresponding analysis passes (or implementing some yourself and hope they're not smarter than the compiler's). –  Apr 27 '11 at 19:49
  • This may or may not answer your second question, but, if your function doesn't do anything after the recursive call, it's tail-recursive. One telltale sign it isn't tail-recursive: you're doing something with the return value of the recursive call, other than returning it. – Daniel Apr 27 '11 at 21:04
  • See also http://stackoverflow.com/questions/806712/how-do-i-know-if-a-function-is-tail-recursive-in-f – Brian Apr 27 '11 at 22:16

3 Answers3

4

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).

Brian
  • 117,631
  • 17
  • 236
  • 300
  • Thanks Brian. Your remark on compilation mode was also helpful. – jliettehk Apr 27 '11 at 20:00
  • 1
    @Brian - would you be able to tell by inspecting the corresponding IL for the function? Also, while a general formal check may be difficult (impossible?), can you give any examples of where it is difficult to tell just by eyeballing? I've seen it said a lot of times that it's not always easy to tell, but I simply have never seen a complex enough tail-recursive function where it wasn't easy to tell. – Stephen Swensen Apr 27 '11 at 20:11
  • 1
    Somewhere I saw a mention that the F# team was considering a future keyword that would let you tell the compiler that you intend a function to be tail-recursive, so the compiler could warn you if it actually is not. That would be really handy, I think. – Joel Mueller Apr 27 '11 at 20:29
  • FWIW, `tailcall` is a reserved word. – Daniel Apr 27 '11 at 21:36
  • 2
    @Stephen - two things that are easy to miss: (1) looking carefully at the call but forgetting that you are in a `try` (e.g. does a `use` at the top of the function negate the tail call? I think so) and (2) when doing mutual recursion where you tail call a function argument that tail calls you back (especially when some args may or may not be partially applied). I don't have examples at-hand, but I know from experience that you can get occasionally surprised if you trust your eyeballs. A much much rarer case is mutual recursion across partial-trust assembly boundaries (which never tail call). – Brian Apr 27 '11 at 22:12
  • (continuing) At the end of the day, what you typically "really" care about is "does my function work properly/performantly on big inputs", in which case there is a very simple way to find out - test it! :) – Brian Apr 27 '11 at 22:13
  • @Brian, yes, a using will 'negate' the tail call, because `use id = exprA in exprB` is equivalent to the function call `using exprA (fun id -> exprB)`, which means `exprB` is evaluted, but then must be passed back to the function `using`, which is itself finally in tail position. – Sebastian Good Apr 28 '11 at 03:40
4

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!)

Sebastian Good
  • 6,310
  • 2
  • 33
  • 57
4

You asked how we can formally check this so I'll have a stab. We first have to define what it means for a function to be tail-recursive. A recursive function definition of the form

let rec f x_1 ... x_n = e

is tail recursive if all calls of f inside e are tail calls - ie. occur in a tail context. A tail context C is defined inductively as a term with a hole []:

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

where e is an F# expression, x is a variable and p is a pattern. We ought to expand this to mutually recursive function definitions but I'll leave that as an exercise.

Lets now apply this to your example. The only call to rec_algo1 in the body of the function is in this context:

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
    []

And since this is a tail context, the function is tail-recursive. This is how functional programmers eyeball it - scan the body of the definition for recursive calls and then verify that each occurs in a tail context. A more intuitive definition of a tail call is when nothing else is done with the result of the call apart from returning it.

petebu
  • 1,827
  • 12
  • 15