ATS: Programming with Theorem-Proving/Tail-call and Tail-recursion
Tail-recursion is of crucial importance for programming in ATS.
Suppose that a function
foo calls a function
bar may be the same one. If the return value of the call to
bar is also the return value of
foo, then this call to
bar is often referred to as a tail-call. If
bar are the same, then this is a (recursive) self tail-call. For instance, there are two recursive calls in the body of the function
f91 defined as follows:
fun f91 (n: int): int = if n >= 101 then n - 10 else f91 (f91 (n+11))
The outer recursive call is a self tail-call while the inner one is not.
If each recursive call in the body of a function is a tail-call, then this function is a tail-recursive function. For instance, the following function
sum2 is tail-recursive:
fun sum2 (n: int, res: int): int = if n > 0 then sum2 (n-1, n+res) else res
In ATS, the single most important optimization is probably the one that turns a self tail-call into a (local) jump. This optimization effectively turns every tail-recursive function into the equivalent of a loop. Although ATS provides direct syntactic support for constructing for-loops and while-loops, the preferred approach to loop construction in ATS is through the use of tail-recursive functions.