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 repeatedly 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.
Multisets (bags) over a given well-founded set S are sets that admit multiple occurrences of elements taken from S. The given ordering on S induces an ordering on the finite multisets over S. This multiset ordering is shown to be well-founded. The multiset ordering enables the use of relatively simple and intuitive termination functions in otherwise difficult termination proofs. In particular, the multiset ordering is used to prove the termination of production systems, programs defined in terms of sets of rewriting rules.
- 1 Dijkstra, E.W. A small note on the additive composition of variant functions. Note EWD592, Burroughs Corp., Neunen, The Netherlands, 1976.Google Scholar
- 2 Floyd, R.W. Assigning meanings to programs. Proc. Symp. in Applied Math., Vol. 19, Amer. Math. Soc., Providence, R.I., pp. 19- 32.Google Scholar
- 3 Gentzen, G. New version of the consistency proof for elementary number theory (1938). In The Collected Papers of Gerhart Gentzen, M.E. Szabo, Ed., North-Holland, Amsterdam, 1969, pp. 252-286.Google Scholar
- 4 Gorn, S. Explicit definitions and linguistic dominoes. Proc. Conf. on Syst. and Comptr. Sci., London, Ontario, Sept. 1965, pp. 77-115.Google Scholar
- 5 Iturriaga, R. Contributions to mechanical mathematics. Ph.D. Th., Carnegie-Mellon U., Pittsburgh, Pa., May 1967.Google Scholar
- 6 Katz, S.M. and Manna, Z. A closer look at termination. Acta Inform. 5, 4 (1975), 333-352.Google ScholarDigital Library
- 7 Knuth, D.E. and Bendix, P.B. Simple word problems in universal algebras. In Computational Problems in Universal Algebras, J. Leech, Ed., Pergamon Press, Oxford, 1969, pp. 263-297,Google Scholar
- 8 Lankford, D.S. Canonical algebraic simplification in computational logic. Memo ATP-25, Automatic Theorem Proving Project, U. of Texas, Austin, Texas, May 1975.Google Scholar
- 9 Lipton, R.J. and Snyder, L. On the halting of tree replacement systems. Proc. Conf. on Theoret. Comptr. Sci., Waterloo, Ontario, Aug. 1977, pp. 43-46.Google Scholar
- 10 Manna, Z. and Ness, S. On the termination of Markov algorithms. Proc. Third Hawaii Int. Conf. on Syst. Sci., Honolulu, Hawaii, Jan. 1970, pp. 789-792.Google Scholar
- 11 Manna, Z. and Waldinger, R.J. Is SOMETIME sometimes better than ALWAYS? Intermittent assertions in proving program correctness. Comm. ACM 21, 2 (Feb. 1978), 159-172. Google ScholarDigital Library
- 12 Plaisted, D. Well-founded orderings for proving the termination of rewrite rules. Memo R-78-932, Dept. of Comptr. Sci., U. of Illinois, Urbana, IlL, July 1978.Google Scholar
- 13 Plaisted, D. A recursively defined ordering for proving termination of term rewriting systems. Memo R-78-943, Dept. of Comptr. Sci., U. of Illinois, Urbana, I11., Oct. 1978.Google Scholar
Index Terms
- Proving termination with multiset orderings
Recommendations
Abstract Relations Between Restricted Termination And Confluence Properties Of Rewrite Systems
We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, and their interrelations. New criteria are ...
Proving termination properties with MU-TERM
AMAST'10: Proceedings of the 13th international conference on Algebraic methodology and software technologyMU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted rewriting, termination of context-...
Comments