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 values of the program variables 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 prove the termination of production systems, programs defined in terms of sets of rewriting rules.
An extended version of this paper appeared as Memo AIM-310, Stanford Artificial Intelligence Laboratory, Stanford, California.
This research was supported in part by the United States Air Force Office of Scientific Research under Grant AFOSR-76-2909 (sponsored by the Rome Air Development Center, Griffiss AFB, NY), by the National Science Foundation under Grant MCS 76-83655, and by the Advanced Research Projects Agency of the Department of Defense under Contract MDA 903-76-C-0206.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Floyd, R. W. [1967], Assigning meanings to programs, Proc. Symp. in Applied Mathematics, vol. 19 (J. T. Schwartz, ed.), American Mathematical Society, Providence, RI, pp. 19–32.
Gentzen, G. [1938], New version of the consistency proof for elementary number theory, The collected papers of Gerhart Gentzen (M. E. Szabo, ed.), North Holland, Amsterdam (1969), pp. 252–286.
Gorn, S. [Sept. 1965], Explicit definitions and linguistic dominoes, Proc. Conf. on Systems and Computer Science, London, Ontario, pp. 77–115.
Iturriaga, R. [May 1967], Contributions to mechanical mathematics, Ph.D. thesis, Carnegie-Mellon Univ., Pittsburgh, PA.
Knuth, D. E. and P. B. Bendix [1969], Simple word problems in universal algebras, Computational Problems in Universal Algebras (J. Leech, ed.), Pergamon Press, Oxford, pp. 263–297.
Lankford, D. S. [May 1975], Canonical algebraic simplification in computational logic, Memo ATP-25, Automatic Theorem Proving Project, Univ. of Texas, Austin, TX.
Lipton, R. J. and L. Snyder [Aug 1977], On the halting of tree replacement systems, Proc. Conf. on Theoretical Computer Science, Waterloo, Ontario, pp. 43–46.
Manna, Z. and S. Ness [Jan 1970], On the termination of Markov algorithms, Proc. Third Hawaii Intl. Conf. on Systems Sciences, Honolulu, HI, pp. 789–792.
Plaisted, D. [July 1978], Well-founded orderings for proving the termination of rewrite rules, Memo R-78-932, Dept. of Computer Science, Univ. of Illinois, Urbana, IL.
Plaisted, D. [Oct. 1978], A recursively defined ordering for proving termination of term rewriting systems, Memo R-78-943, Dept. of Computer Science, Univ. of Illinois, Urbana, IL.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N., Manna, Z. (1979). Proving termination with multiset orderings. In: Maurer, H.A. (eds) Automata, Languages and Programming. ICALP 1979. Lecture Notes in Computer Science, vol 71. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09510-1_15
Download citation
DOI: https://doi.org/10.1007/3-540-09510-1_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09510-1
Online ISBN: 978-3-540-35168-9
eBook Packages: Springer Book Archive