Termination-Checking for Recursive Functions

There is a mechanism in ATS that allows the programmer to supply termination metrics for checking whether recursively defined functions are terminating. It will soon become clear that this mechanism of termination-checking plays a fundamental role in the design of ATS/LF, a theorem-proving subsystem of ATS, where proofs are constructed as total functional programs.

A termination metric is just a tuple of natural numbers and the standard lexicographic ordering on natural numbers is used to order such tuples. In the following example, a singleton metric n is supplied to verify that the recursive function fact is terminating, where n is the value of the integer argument of fact:

fun fact {n:nat} .<n>. (x: int n): int = if x > 0 then x * fact (x-1) else 1 // end of [fact]

Note that the metric attached to the recursive call fact(x-1) is n-1, which is strictly less than the initial metric n. Essentially, termination-checking in ATS verifies that the metric attached to each recursive call in the body of a function is strictly less that the initial metric attached to the function.

A more difficult and also more interesting example is given as follows, where the MacCarthy's 91-function is implemented:

fun f91 {i:int} .<max(101-i,0)>. (x: int i) : [j:int | (i < 101 && j==91) || (i >= 101 && j==i-10)] int (j) = if x >= 101 then x-10 else f91 (f91 (x+11)) // end of [f91]

The metric supplied to verify the termination of f91 is max(101-i,0), where i is the value of the integer argument of f91. Please try to verify manually that this metric suffices for verifying the termination of f91.

As another example, the following code implements the Ackermann's function, which is well-known for being recursive but not primitive recursive:

fun acker {m,n:nat} .<m,n>. (x: int m, y: int n): Nat = if x > 0 then if y > 0 then acker (x-1, acker (x, y-1)) else acker (x-1, 1) else y + 1 // end of [acker]

The metric supplied for verifying the termination of acker is a pair (m,n), where m and n are values of the two integer arguments of acker. The metrics attached to the three recursive calls to acker are, from left to right, (m-1,k) for some natural number k, (m,n-1), and (m-1,1). Clearly, these metrics are all strictly less than the initial metric (m,n) according to the lexicographic ordering on pairs of natural numbers.

Termination-checking for mutually recursive functions is similar. In the following example, isevn and isodd are defined mutually recursively:

fun isevn {n:nat} .<2*n>. (n: int n) : bool = if n = 0 then true else isodd (n-1) and isodd {n:nat} .<2*n+1>. (n: int n) : bool = not (isevn (n))

The metrics supplied for verifying the termination of isevn and isodd are 2*n and 2*n+1, respectively, where n is the value of the integer argument of isevn and also the value of the integer argument of isodd. Clearly, if the metrics (n, 0) and (n, 1) are supplied for isevn and isodd, respectively, the termination of these two functions can also be verified. Note that it is required that the metrics for mutually recursively defined functions be tuples of the same length.