A Tutorial on Programming Features in ATS:
<<< PreviousNext >>>

Mutual Tail-Recursion

Mutually tail-recursive functions are commonly encountered in practice. Assume that foo and bar are two mutually defined functions. In the body of either foo or bar, a tail-call to foo or bar is referred to as a mutually tail-recursive call. If every call to foo or bar in the bodies of foo and bar are tail-call, then foo and bar are mutually tail-recursive. Mutual recursion involving more functions can be defined similarly. As an example, the following two functions isEvn and isOdd are defined mutually recursively: 

fun isEvn (n: int): bool = if n > 0 then isOdd (n-1) else true
and isOdd (n: int): bool = if n > 0 then isEvn (n-1) else false

The call to isOdd in the body of isEvn is a mutually tail-recursive call, and the call to isEvn in the body of isOdd is also a a mutually tail-recursive call. Therefore, isEvn and isOdd are mutually tail-recursive.

In order to turn mutually recursive tail-calls into jumps, the bodies of the involved mutually recursive functions need to be combined. The keyword fn* in ATS is introduced for this purpose precisely. For instance, let us replace fun with fn* in the code above: 

fn* isEvn (n: int): bool = if n > 0 then isOdd (n-1) else true
and isOdd (n: int): bool = if n > 0 then isEvn (n-1) else false

Then the following C code is essentially generated from compiling these two mutually defined functions: 

bool isEvnisOdd (int tag, int n) {

bool res ;

switch (tag) {
  0: goto isEvn ;
  1: goto isOdd ;
  default : exit (1) ;
}

isEvn: if (n > 0) { n = n - 1; goto isodd; } else { res = true; goto done; }
isOdd: if (n > 0) { n = n - 1; goto isEvn; } else { res = false; goto done; }

done: return res ;

} /* end of [isEvnisOdd] */

bool isEvn (int n) { return isEvnisOdd (0, n) ; }
bool isOdd (int n) { return isEvnisOdd (1, n) ; }

Note that mutually recursive functions can be combined in such a manner only if they all have the same return type. In the above case, both isEvn and isOdd have the same return type bool.

When translating C code involving embedded loops, we often encounter the need for mutual tail-recursion. For instance, the following C code prints out ordered pairs of digits: 

int main (
  int argc, char *argv[]
) {
  int i, j ;
  for (i = 0; i <= 9; i += 1) {
    for (j = i; j <= 9; j += 1) {
      if (i < j) printf (", ") ; printf ("(%i, %i)", i, j) ;
    } /* for */
    printf ("
") ;
  } /* for */
  return 0 ;
}

A straightforward translation of the C code into ATS (in the style of functional programming) can be done as follows: 

implement
main (argc, argv) = let
  fn* loop1
    {i:nat | i <= 10} (i: int i): void =
    if i <= 9 then loop2 (i, i) else ()
  // end of [loop1]

  and loop2
    {i,j:nat | i <= 9; j <= 10} (i: int i, j: int j): void =
    if j <= 9 then (
      if i < j then (
        print ", "; printf ("(%i, %i)", @(i, j)); loop2 (i, j+1)
      ) // end of [if]
    ) else (
      print_newline (); loop1 (i+1)
    ) // end of [if]
  // end of [loop2]
in
  loop1 (0)
end // end of [main]

Evidently, loop1 and loop2 are defined mutually tail-recursively. The use of the keyword fn* ensures that these two functions are translated into the equivalent of two loops in C, which require only a fixed amount of stack space to run.

<<< PreviousHomeNext >>>
Tail-Recursive Call OptimizationUpMetrics for Termination Verification