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