Advertisement

Termination analysis by inductive evaluation

  • Jürgen Brauburger
  • Jürgen Giesl
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

Abstract

We present a new approach for automatic termination analysis of functional programs. Several methods have been presented which try to find a well-founded ordering such that the arguments in the recursive calls are smaller than the corresponding inputs. However, previously developed approaches for automated termination analysis often disregard the conditions under which the recursive calls are evaluated. Hence, the existing methods fail for an important class of algorithms where the necessary information for proving termination is ‘hidden’ in the conditions. In this paper we develop the inductive evaluation method which analyzes the auxiliary functions occurring in the conditions of the recursive calls. We also discuss an extension of our method to partial functions in order to determine their domains automatically. The proposed technique proved successful for termination analysis of numerous algorithms in functional as well as imperative programming languages.

Keywords

Partial Function Recursive Call Inductive Evaluation Termination Proof Imperative Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AG97]
    T. Arts and J. Giesl. Proving innermost normalisation automatically. In Proc. RTA-97, Sitges, Spain, LNCS 1232, 1997.Google Scholar
  2. [BM79]
    R. S. Boyer and J S. Moore. A computational logic. Academic Press, 1979.Google Scholar
  3. [BR95]
    A. Bouhoula and M. Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 14:189–235, 1995.MathSciNetCrossRefzbMATHGoogle Scholar
  4. [BG96]
    J. Brauburger and J. Giesl. Termination analysis for partial functions. In Proc. 3rd Int. Static Analysis Symp., Aachen, Germany, LNCS 1145, 1996. Extended version appeared as Report IBN-96-33, TU Darmstadt, 1996.Google Scholar
  5. [BG98]
    J. Brauburger and J. Giesl. Termination analysis with inductive evaluation. Technical Report IBN-98-47, TU Darmstadt, Germany, 1998.Google Scholar
  6. [Bra97]
    J. Brauburger. Automatic termination analysis for partial functions using polynomial orderings. In Proc. 4th SAS, Paris, France, LNCS 1302, 1997.Google Scholar
  7. [Bun+89]
    A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, and A. Stevens. A rational reconstruction and extension of recursion analysis. In Proc. IJCAI '89, Detroit, USA, 1989.Google Scholar
  8. [Der87]
    N. Dershowitz. Termination of rewriting. J. Symb. Comp., 3:69–115, 1987.zbMATHMathSciNetCrossRefGoogle Scholar
  9. [Gie95a]
    J. Giesl. Generating polynomial orderings for termination proofs. In Proc. RTA-95, Kaiserslautern, Germany, LNCS 914, 1995.Google Scholar
  10. [Gie95b]
    J. Giesl. Automatisierung von Terminierungsbeweisen für rekursiv definierte Algorithmen. PhD thesis, Infix-Verlag, St. Augustin, Germany, 1995.Google Scholar
  11. [Gie95c]
    J. Giesl. Termination analysis for functional programs using term orderings. In Proc. 2nd Int. Static Analysis Symp., Glasgow, UK, LNCS 983, 1995.Google Scholar
  12. [Gie97]
    J. Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning, 19:1–29, 1997.zbMATHMathSciNetCrossRefGoogle Scholar
  13. [GWB98]
    J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P. Schmitt, editors, Automated Deduction — A Basis for Applications, vol. 3. Kluwer Academic Publishers, 1998.Google Scholar
  14. [Gri81]
    D. Gries. The science of programming. Springer-Verlag, New York, 1981.zbMATHGoogle Scholar
  15. [Hen80]
    P. Henderson. Functional programming. Prentice-Hall, London, 1980.zbMATHGoogle Scholar
  16. [HS96]
    D. Hutter and C. Sengler. INKA: The next generation. In Proc. CADE-13, New Brunswick, USA, LNAI 1104, 1996.Google Scholar
  17. [KZ95]
    D. Kapur and H. Zhang. An overview of Rewrite Rule Laboratory (RRL). J. Computer Math. Appl., 29:91–114, 1995.MathSciNetCrossRefGoogle Scholar
  18. [Lan79]
    D.S. Lankford. On proving term rewriting systems are noetherian. Memo MTP-3, Math. Dept., Louisiana Tech. Univ., Ruston, USA, 1979.Google Scholar
  19. [NN96]
    F. Nielson and H. R. Nielson. Operational semantics of termination types. Nordic Journal of Computing, 3(2):144–187, 1996.MathSciNetzbMATHGoogle Scholar
  20. [PS97]
    S. E. Panitz and M. Schmidt-Schau\. TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In Proc. 4th Int. Static Analysis Symp., Paris, France, LNCS 1302, 1997.Google Scholar
  21. [Plü90]
    L. Plümer. Termination proofs for logic programs. LNAI 446, 1990.Google Scholar
  22. [Pro96]
    M. Protzen. Patching faulty conjectures. In Proc. CADE-13, LNAI 1104, New Brunswick, USA, 1996.Google Scholar
  23. [SD94]
    D. De Schreye and S. Decorte. Termination of logic programs: The never-ending story. Journal of Logic Programming, 19/20:199–260, 1994.CrossRefGoogle Scholar
  24. [Sen96]
    C. Sengler. Termination of algorithms over non-freely generated data types. In Proc. CADE-13, New Brunswick, USA, LNAI 1104, 1996.Google Scholar
  25. [Ste94]
    J. Steinbach. Generating polynomial orderings. IPL, 49:85–93, 1994.zbMATHCrossRefGoogle Scholar
  26. [Ste95]
    J. Steinbach. Simplification orderings: History of results. Fundamenta Informaticae, 24:47–87, 1995.zbMATHMathSciNetGoogle Scholar
  27. [UvG88]
    J. D. Ullman and A. van Gelder. Efficient tests for top-down termination of logical rules. Journal of the ACM, 35(2):345–373, 1988.CrossRefGoogle Scholar
  28. [Wal94a]
    C. Walther. Mathematical induction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2. Oxford University Press, 1994.Google Scholar
  29. [Wal94b]
    C. Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71(1):101–157, 1994.zbMATHMathSciNetCrossRefGoogle Scholar
  30. [ZKK88]
    H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In Proc. CADE-9, Argonne, USA, LNCS 310, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Jürgen Brauburger
    • 1
  • Jürgen Giesl
    • 1
  1. 1.FB InformatikTU DarmstadtDarmstadtGermany

Personalised recommendations