A Tutorial on Programming Features in ATS: | ||
---|---|---|

<<< Previous | Next >>> |

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_{1}, ..., M_{n}) of natural
numbers, where n >= 0. We use the standard well-founded lexicographical
ordering on natural numbers to order such tuples.

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

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.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] |

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] |

(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.

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:

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.Suppose that foo and bar are declared as follows:

Moreover, suppose that the following implementation of foo is given in a file named foo.dats: while the following implementation of bar is given in another file named bar.dats: 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<<< Previous | Home | Next >>> |

Mutual Tail-Recursion | Up | Higher-Order Functions |