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:
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]
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]
Termination-checking for mutually recursive functions is similar. In the following example, isevn and isodd are defined mutually recursively:
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.