Termination analysis for partial functions

  • Jürgen Brauburger
  • Jürgen Giesl
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


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.


Logic Program Partial Function Recursive Call Total Function Termination Proof 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BG96]
    J. Brauburger & J. Giesl. Termination Analysis for Partial Functions. Technical Report IBN 96/33, TH Darmstadt, 1996. Available from http://kirmes. Scholar
  2. [Bi86]
    [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. [BM79]
    R. S. Boyer & J S. Moore. A Computational Logic. Academic Press, 1979.Google Scholar
  4. [BM88]
    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. [BU90]
    [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. [Der87]
    N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1, 2):69–115, 1987.Google Scholar
  7. [Gie95a]
    J. Giesl. Generating Polynomial Orderings for Termination Proofs. Pr. 6th Int. Conf. Rewr. Tech. & App., LNCS 914, Kaiserslautern, Germany, 1995.Google Scholar
  8. [Gie95b]
    J. Giesl. Automated Termination Proofs with Measure Functions. In Proc. 19th Annual German Conf. on AI, LNAI 981, Bielefeld, Germany, 1995.Google Scholar
  9. [Gie95c]
    J. Giesl. Termination Analysis for Functional Programs using Term Orderings. Pr. 2nd Int. Stat. Analysis Symp., LNCS 983, Glasgow, Scotland, 1995.Google Scholar
  10. [Gie96]
    J. Giesl. Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning, 1996. To appear.Google Scholar
  11. [Hen80]
    P. Henderson. Functional Programming. Prentice-Hall, London, 1980.Google Scholar
  12. [Hol91]
    C. K. Holst. Finiteness Analysis. In Proc. 5th ACM Conf. Functional Prog. Languages & Comp. Architecture, LNCS 523, Cambridge, MA, USA, 1991.Google Scholar
  13. [Man74]
    Z. Manna. Mathematical Theory of Computation. McGraw-Hill, 1974.Google Scholar
  14. [NN95]
    F. Nielson & H. R. Nielson. Termination Analysis based on Operational Semantics. Technical Report, Aarhus University, Denmark, 1995.Google Scholar
  15. [Plü90]
    L. Plümer. Termination Proofs for Logic Programs. LNAI 446, Springer-Verlag, 1990.Google Scholar
  16. [SD94]
    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. [Ste95]
    J. Steinbach. Simplification Orderings: History of Results. Fundamenta Informaticae 24:47–87, 1995.Google Scholar
  18. [UV88]
    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. [Wal88]
    C. Walther. Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. In Proc. 9th CADE, LNCS 310, Argonne, IL, 1988.Google Scholar
  20. [Wal94a]
    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. [Wal94b]
    C. Walther. On Proving the Termination of Algorithms by Machine. Artificial Intelligence, 71(1):101–157, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

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

Personalised recommendations