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