Skip to main content
SpringerLink
Log in

Termination analysis for partial functions

  • Contributed Papers
  • Conference paper
  • First Online:
Static Analysis (SAS 1996)

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

Included in the following conference series:

Abstract

This paper deals with automated termination analysis for partial functional programs, i.e. for functional programs which do not terminate for each input. We present a method to determine their domains (resp. non-trivial subsets of their domains) automatically. More precisely, for each functional program a termination predicate algorithm is synthesized, which only returns true for inputs where the program is terminating. To ease subsequent reasoning about the generated termination predicates we also present a procedure for their simplification.

This work was supported by the Deutsche Forschungsgemeinschaft under grant no. Wa 652/7-1 as part of the focus program “Deduktion∝.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Brauburger & J. Giesl. Termination Analysis for Partial Functions. Technical Report IBN 96/33, TH Darmstadt, 1996. Available from http://kirmes. inferenzsysteme.informatik.th-darmstadt.de/~report/ibn-96-33.ps.gz.

    Google Scholar 

  2. [Bi+86] S. Biundo, B. Hummel, D. Hutter & C. Walther. The Karlsruhe Induction Theorem Proving System. Pr. 8th CADE, LNCS 230, Oxford, England, 1986.

    Google Scholar 

  3. R. S. Boyer & J S. Moore. A Computational Logic. Academic Press, 1979.

    Google Scholar 

  4. R. S. Boyer & J. S. Moore. The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. Journal of Automated Reasoning, 4:117–172, 1988.

    Google Scholar 

  5. [Bu+90] A. Bundy, F. van Harmelen, C. Horn & A. Smaill. The Oyster-Clam System. In Proc. 10th CADE, LNAI 449, Kaiserslautern, Germany, 1990.

    Google Scholar 

  6. N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1, 2):69–115, 1987.

    Google Scholar 

  7. J. Giesl. Generating Polynomial Orderings for Termination Proofs. Pr. 6th Int. Conf. Rewr. Tech. & App., LNCS 914, Kaiserslautern, Germany, 1995.

    Google Scholar 

  8. J. Giesl. Automated Termination Proofs with Measure Functions. In Proc. 19th Annual German Conf. on AI, LNAI 981, Bielefeld, Germany, 1995.

    Google Scholar 

  9. J. Giesl. Termination Analysis for Functional Programs using Term Orderings. Pr. 2nd Int. Stat. Analysis Symp., LNCS 983, Glasgow, Scotland, 1995.

    Google Scholar 

  10. J. Giesl. Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning, 1996. To appear.

    Google Scholar 

  11. P. Henderson. Functional Programming. Prentice-Hall, London, 1980.

    Google Scholar 

  12. C. K. Holst. Finiteness Analysis. In Proc. 5th ACM Conf. Functional Prog. Languages & Comp. Architecture, LNCS 523, Cambridge, MA, USA, 1991.

    Google Scholar 

  13. Z. Manna. Mathematical Theory of Computation. McGraw-Hill, 1974.

    Google Scholar 

  14. F. Nielson & H. R. Nielson. Termination Analysis based on Operational Semantics. Technical Report, Aarhus University, Denmark, 1995.

    Google Scholar 

  15. L. Plümer. Termination Proofs for Logic Programs. LNAI 446, Springer-Verlag, 1990.

    Google Scholar 

  16. D. De Schreye & S. Decorte. Termination of Logic Programs: The Never-Ending Story. Journal of Logic Programming 19,20:199–260, 1994.

    Google Scholar 

  17. J. Steinbach. Simplification Orderings: History of Results. Fundamenta Informaticae 24:47–87, 1995.

    Google Scholar 

  18. J. D. Ullman & A. van Gelder. Efficient Tests for Top-Down Termination of Logical Rules. Journal of the ACM, 35(2):345–373, 1988.

    Google Scholar 

  19. C. Walther. Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. In Proc. 9th CADE, LNCS 310, Argonne, IL, 1988.

    Google Scholar 

  20. C. Walther. Mathematical Induction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, Oxford University Press, 1994.

    Google Scholar 

  21. C. Walther. On Proving the Termination of Algorithms by Machine. Artificial Intelligence, 71(1):101–157, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB Informatik, TH Darmstadt, Alexanderstr. 10, 64283, Darmstadt, Germany

    Jürgen Brauburger & Jürgen Giesl

Authors
  1. Jürgen Brauburger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Radhia Cousot David A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brauburger, J., Giesl, J. (1996). Termination analysis for partial functions. In: Cousot, R., Schmidt, D.A. (eds) Static Analysis. SAS 1996. Lecture Notes in Computer Science, vol 1145. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61739-6_37

Download citation

  • DOI: https://doi.org/10.1007/3-540-61739-6_37

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61739-6

  • Online ISBN: 978-3-540-70674-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation