Termination Metrics


In ATS, the programmer is allowed to supply termination metrics for verifing the termination of recursively defined functions. This is really an indispensable feature for supporting programming with theorem proving as proof functions, namely, functions representing proofs, must be proven to be pure and terminating.

A termination metric is a tuple (M1, ..., Mn) of natural numbers, where n >= 0 . We use the standard well-founded lexicographical ordering on natural numbers to order such tuples.

A Primitive Recursive Function

The kind of recursion in the following implementation of the factorial function is primitive recursion:
// [fact] implements the factorial function
fun fact {n:nat} .< n >. (n: int n): Int = if n > 0 then n * fact (n-1) else 1
The syntax .< n >. indicates that the metric supplied for verifying the termination of the defined function is a singleton tuple (n). In the definition of fact, the metric for the recursive call to fact is (n-1), which is strictly less than (n). So the function fact is terminating.

Some General Recursive Functions

We implement as follows a function gcd that computes the greatest common division of two given positive integers:
// [gcd] computes the greates common divisors of two positive integers
fun gcd {m,n:int | m > 0; n > 0} .< m+n >.
  (m: int m, n: int n): [r:nat | 1 <= r; r <= min(m, n)] int r =
  if m > n then gcd (m - n, n)
  else if m < n then gcd (m, n - m)
  else m
The syntax .< m+n >. indicates that the termination metric (m+n) should be used to verify that the defined function gcd is terminating. In the definition of gcd, the termination metric for the first recursive call to gcd is (m-n)+n=m, which is strictly less than the original termination metri m+n (as n is positive); the termination metric for the second recursive call to gcd is m+(n-m)=n, which is also strictly less than the original termination metric m+n (as m is positive). Thus, gcd is a terminating function.

As another example, we implement as follows the Ackermann's function:

// [ack] implements the Ackermann's function
fun ack {m,n:nat} .< m, n >.
  (m: int m, n: int n): Nat =
  if m > 0 then
    if n > 0 then ack (m-1, ack (m, n-1)) else ack (m-1, 1)
  else n+1
The syntax .< m, n >. indicates that the termination metric is a pair of natural numbers: (m, n). We use the lexicographical ordering on natural numbers to compare such metrics. To verify that ack is terminating, we need to solve the following constraints: As all of these constraints can be readily solved, we conclude that ack is a terminating funciton.

Mutually Recursive Functions

When mutually recursive functions are to be verified, the termination metrics for these functions, which are tuples of natural numbers, must be of the same tuple length. We given a simple example as follows:
// mutually recursive functions
fun isEven {n:nat} .< 2*n+2 >. (n: int n): bool =
  if n > 0 then ~(isOdd n) else true
and isOdd {n:nat} .< 2*n+1 >. (n: int n): bool =
  if n > 0 then isEven (n-1) else false
Clearly, we may also verify the termination of these two functions by using the metrics .< n, 1 >. and .< n, 0 >. for isEven and isOdd, respectively.

The code used for illustration is available here.