Report Number: CS-TR-78-651
Institution: Stanford University, Department of Computer Science
Title: Proving termination and multiset orderings
Author: Dershowitz, Nachum
Author: Manna, Z ohar
Date: March 1978
Abstract: A common tool for proving the termination of programs is the well-founded set, a set ordered in such a way as to admit no infinite descending sequences. The basic approach is to find a termination function that maps the elements of the program into some well-founded set, such that the value of the termination function is continually reduced throughout the computation. All too often, the termination functions required are difficult to find and are of a complexity out of proportion to the program under consideration. However, by providing more sophisticated well-founded sets, the corresponding termination functions can be simplified. Given a well-founded set S, we consider multisets over S, "sets" that admit multiple occurrences of elements taken from S. We define an ordering on all finite multisets over S that is induced by the given ordering on S. This multiset ordering is shown to be well-founded. The value of the multiset ordering is that it permits the use of relatively simple and intuitive termination functions in otherwise difficult termination proofs. In particular, we apply the multiset ordering to provide simple proofs of the termination of production systems, programs defined in terms of sets of rewriting rules.
http://i.stanford.edu/pub/cstr/reports/cs/tr/78/651/CS-TR-78-651.pdf