A Tutorial on Programming Features in ATS:
<<< Previous		Next >>>

Metrics for Termination Verification

ATS provides a simple means for the programmer to verify the termination of recursively defined functions by supplying proper termination metrics. This is an indispensable feature for supporting the paradigm of programming with theorem-proving as proof functions, namely, functions representing proofs, must be proven to be terminating.

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

Primitive Recursion

The kind of recursion in the following implementation of the factorial function is primitive recursion:

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

The special 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). Therefore, the defined function fact is terminating.

General Recursion

We implement as follows a function gcd that computes the greatest common division of two given positive integers:

//
// computing the greatest common divisors of two positive ints
//
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
// end of [gcd]

The syntax .<m+n>. indicates that the termination metric (m+n) is supplied 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, which is famous for being recursive but not primitive recursion:

//
// [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 // end of [if]
// end of [ack]

The syntax .<m, n>. indicates that the termination metric is a pair of natural numbers: (m, n). Note that the standard 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.

Mutual Recursion

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:

fun isEvn
  {n:nat} .<2*n+2>. (n: int n): bool =
  if n > 0 then ~(isOdd n) else true // end of [if]
// end of [isEvn]

and isOdd
  {n:nat} .<2*n+1>. (n: int n): bool =
  if n > 0 then isEvn (n-1) else false // end of [if]
// end of [isOdd]

Clearly, we can also verify the termination of these two functions by using the metrics .<n, 1>. and .<n, 0>. for isEvn 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 to resolve this issue of calling cycles among functions by solely relying on termination metrics. Instead, atscc can generate run-time code for detecting calling cycles among 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.

<<< Previous	Home	Next >>>
Mutual Tail-Recursion	Up	Higher-Order Functions