## Andreas Abel

### Termination of Mutually Recursive Functions

A recursive function terminates if in each recursive call the argument
is decreased wrt. a given measure in a well-founded domain. That can
easily be proven constructively by wellfounded induction over the
measure of the argument.
Straightforward extension of this criterion ("each call is decreasing")
to mutually recursive functions is too strict. It is sufficient that
whenever the same function appears in a call sequence, then the argument
is decreased. The classical proof for the latter statement is still
simple, but the constructive proof requires an additional wellordering
on the function symbols.

First the notions of a call graph and its goodness are introduced for
mutually recursive functions with one argument, then the harder case for
functions with several arguments. A constructive proof is given for the
first case and a sketch for the second.

The results are applicable for all pure functional programming languages
and also for term rewriting systems and implementations of type-theory.

May 26, 2000

3:30pm

Wean 8220