Abstract
Size-change termination (SCT) automatically identifies termination of first-order functional programs. The SCT principle: a program terminates if every infinite control flow sequence would cause an infinite descent in a well-founded data value (POPL 2001).
More recent work (RTA 2004) developed a termination analysis of the pure untyped λ-calculus using a similar approach, but an entirely different notion of size was needed to compare higher-order values. Again this is a powerful analysis, even proving termination of certain λ-expressions containing the fixpoint combinator Y. However the language analysed is tiny, not even containing constants.
These techniques are unified and extended significantly, to yield a termination analyser for higher-order, call-by-value programs as in ML’s purely functional core or similar functional languages. Our analyser has been proven correct, and implemented for a substantial subset of OCaml.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avery, J.: Size-change termination for programs with non-well-founded data. Graduate project, University of Copenhagen
Bird, R.: Using circular programs to eliminate multiple traversals of data. Acta Informatica 21, 239–250 (1984)
Danvy, O.: Lambda-lifting in quadratic time. In: Hu, Z., Rodríguez-Artalejo, M. (eds.) FLOPS 2002. LNCS, vol. 2441, pp. 134–151. Springer, Heidelberg (2002)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
Johnsson, T.: Lambda lifting: transforming programs to recursive equations. In: Proceedings of a conference on Functional Programming languages and Computer Architecture. Springer, Heidelberg (1985)
Jones, N.D., Bohr, N.: Termination analysis of the untyped λ-calculus. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 1–23. Springer, Heidelberg (2004)
Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6, 308–320 (1964)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the 28th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languagaes, pp. 81–92. ACM Press, New York (2001)
Leroy, X.: The Objective Caml System: Documentation and User’s Manual (2004)
Lindenstrauss, N., Sagiv, Y.: Automatic termination analysis of prolog programs. In: Proceedings of the Fourteenth International Conference on Logic Programming, pp. 64–67 (1997)
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)
Peyton-Jones, S.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)
Sereni, D.: Higher-order size-change termination analyser (2004), Available at http://web.comlab.ox.ac.uk/oucl/work/damien.sereni/hoterm.tar.gz
Sereni, D.: Termination analysis of higher-order functional programs. Technical Report PRG-RR-04-20, Oxford University Computing Laboratory (2004), http://web.comlab.ox.ac.uk/oucl/publications/tr/rr-04-20.html
Shivers, O.: Control-flow analysis in scheme. In: Proceedings of the SIGPLAN 1988 Conference on Programming Language Design and Implementation, June 1988, pp. 164–174 (1988)
Shivers, O.: Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University (May 1991)
Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, Institut für Informatik der Technischen Universität München (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sereni, D., Jones, N.D. (2005). Termination Analysis of Higher-Order Functional Programs. In: Yi, K. (eds) Programming Languages and Systems. APLAS 2005. Lecture Notes in Computer Science, vol 3780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11575467_19
Download citation
DOI: https://doi.org/10.1007/11575467_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29735-2
Online ISBN: 978-3-540-32247-4
eBook Packages: Computer ScienceComputer Science (R0)