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, where foo and 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 foo and 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.