Skip to main content
SpringerLink
Log in

On Automating Inductive and Non-inductive Termination Methods

  • Conference paper
  • First Online:
Advances in Computing Science — ASIAN’99 (ASIAN 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1742))

Included in the following conference series:

Abstract

The Coq and ProPre systems show the automated termination of a recursive function by first constructing a tree associated with the specification of the function which satisfies a notion of terminal property and then verifying that this construction process is formally correct. However, those two steps strongly depend on inductive principles and hence Coq and ProPre can only deal with the termination proofs that are inductive. There are however many functions for which the termination proofs are non-inductive. In this article, we attempt to extend the class of functions whose proofs can be done automatically à la Coq and ProPre to a larger class including functions whose termination proofs are not inductive. We do this by extending the terminal property notion and replacing the verification step above by one that searches for a decreasing measure which can be used to establish the termination of the function.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail in Proceeding TAPSOFT’97, LNCS, volume 1214, 261–272.

    Google Scholar 

  2. T. Arts and J. Giesl. Proving innermost normalisation automatically in Proceeding RTA’97, LNCS, volume 1232, 157–171.

    Google Scholar 

  3. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9(2),137–159, 1987.

    MATH  Google Scholar 

  4. C. Cornes et al.. The Coq proof assistant reference manual version 5.10. Technical Report 077, INRIA, 1995.

    Google Scholar 

  5. N. Dershowitz. Termination of rewriting. Theoretical Computer Science 17, 279–301,1982.

    Google Scholar 

  6. N. Dershowitz and C. Hoot. Natural termination. Theoretical Computer Science142(2), 179–207, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  7. J. Dick, J. Kalmus and U. Martin. Automating the Knuth Bendix ordering. Acta Informatica 28, 95–119, 1990.

    Google Scholar 

  8. T. Genet and I. Gnaedig. Termination proofs using gpo ordering constraints. TAP-SOFT, LNCS 1214, 249–260, 1997.

    Article  Google Scholar 

  9. J. Giesl. Generating polynomial orderings for termination proofs. Proceedings of the 6th International Conference on Rewriting Techniques and Application, Kaiserlautern, LNCS, volume 914, 1995.

    Google Scholar 

  10. F. Kamareddine and F. Monin. On formalised proofs of termination of recursive functions. In Proc. International Conference on Principles and Practice of Declar-ative Programming, Paris, France, 1999.

    Google Scholar 

  11. F. Kamareddine and F. Monin. Induction Lemmas for Termination of Recursive Functions in a Typed System Proc. submitted.

    Google Scholar 

  12. D. E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational problems in abstract algebra, Pergamon Press, 263–297,1970.

    Google Scholar 

  13. T. Kolbe. Challenge problems for automated termination proofs of term rewriting systems. Technical Report IBN96-42, Technische Hochshule Darmstadt, Alexanderstr.10, 64283 Darmstadt, Germany, 1996.

    Google Scholar 

  14. P. Lescanne. On the recursive decomposition ordering with lexicographical status and other related orderings. Journal of Automated Reasoning 6(1) 39–49, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  15. P. Manoury. A User’s friendly syntax to define recursive functions as typed lambda-terms. Proceedings of Type for Proofs and Programs TYPES’94, LNCS, volume 996,1994.

    Google Scholar 

  16. P. Manoury and M. Simonot. Des preuves de totalit_e de fonctions comme synth_ese de programmes. PhD thesis, University Paris 7, 1992.

    Google Scholar 

  17. P. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science 135(2) 319–343, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  18. A. Middeldorp and H. Zantema. Simple termination of rewrite systems. Theoretical Computer Science 175, 127–158, 1997.

    Google Scholar 

  19. F. Monin and M. Simonot. An ordinal measure based procedure for termination of functions. To appear in Theoretical Computer Science.

    Google Scholar 

  20. M. Parigot. Recursive programming with proofs. Theoretical Computer Science94(2) 335–356, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  21. J. Steinbach. Generating polynomial orderings. Information Processing Letters 49,85–93, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Electrical Engineering, Heriot-Watt University, Edinburgh, EH14 4AS, Scotland

    Fairouz Kamareddine & François Monin

Authors
  1. Fairouz Kamareddine
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. François Monin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, Chennai, 600 017, India

    P. S. Thiagarajan

  2. School of Computing, National University of Singapore, Lower Kent Ridge Road, Singapore, 119260

    Roland Yap

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kamareddine, F., Monin, F. (1999). On Automating Inductive and Non-inductive Termination Methods. In: Thiagarajan, P.S., Yap, R. (eds) Advances in Computing Science — ASIAN’99. ASIAN 1999. Lecture Notes in Computer Science, vol 1742. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46674-6_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-46674-6_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66856-5

  • Online ISBN: 978-3-540-46674-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation