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:

(m-1, k) is less than (m, n) under the assumption m > 0, where k is an arbitrary natural number.
(m, n-1) is less than (m, n) under the assumption m > 0 and n > 0.
(m-1, 1) is less than (m, n) under the assumption m > 0.

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.

Termination Checking at Run-time

Suppose that foo and bar are declared as follows:

fun foo ():<> void and bar ():<> void

Moreover, suppose that the following implementation of foo is given in a file named foo.dats:

implement foo () = $Bar.bar ()

while the following implementation of bar is given in another file named bar.dats:

implement bar () = $Foo.foo ()

Clearly, neither foo nor bar is terminating. In practice, it is difficult resolve this issue of calling cycles among terminating functions by solely relying on termination metrics. Instead, atscc can generate run-time code for detecting calling cycles among terminating functions if the flag -D_ATS_TERMINATION_CHECK is present. For instance, if foo.dats and bar.dats are compiled as follows:

atscc -D_ATS_TERMINATION_CHECK foo.dats and bar.dats

then a run-time error is to be reported to indicate a calling cycle when either foo.dats or bar.dats is loaded dynamically.

The code used for illustration is available here.