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.
// [fact] implements the factorial function fun fact {n:nat} .< n >. (n: int n): Int = if n > 0 then n * fact (n-1) else 1The 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.
// [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 mThe 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+1The 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:
// 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 falseClearly, 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.