Abstract
An algorithm is developed that, given an untyped λ-expression, can certify that its call-by-value evaluation will terminate. It works by an extension of the ”size-change principle” earlier applied to first-order programs. The algorithm is sound (and proven so in this paper) but not complete: some λ-expressions may in fact terminate under call-by-value evaluation, but not be recognised as terminating.
The intensional power of size-change termination is reasonably high: It certifies as terminating all primitive recursive programs, and many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson’s ”minimum” algorithm. Further, the approach allows free use of the Y combinator, and so can identify as terminating a substantial subset of PCF.
The extensional power of size-change termination is the set of functions computable by size-change terminating programs. This lies somewhere between Péter’s multiple recursive functions and the class of ε 0-recursive functions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Frederiksen, C.C., Jones, N.D.: Running-time Analysis and Implicit Complexity. Submitted to Journal of Automated reasoningJournal dadada
Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)
Jones, N.D., Nielson, F.: Abstract Interpretation: a Semantics-Based Tool for Program Analysis. In: Handbook of Logic in Computer Science, pp. 527–629. Oxford University Press, Oxford (1994)
Jones, N.D., Glenstrup, A.: Partial Evaluation Termination Analysis and Specialization-Point Insertion. ACM Transactions on Programming Languages and Systems (2004)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The Size-Change Principle for Program Termination. In: POPL 2001: Proceedings 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (January 2001)
Lee, C.S.: Finiteness analysis in polynomial time. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 493–508. Springer, Heidelberg (2002)
Lee, C.S.: Program termination analysis in polynomial time. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol. 2487, pp. 218–235. Springer, Heidelberg (2002)
Lee, C.S.: Program Termination Analysis and the Termination of Offline Partial Evaluation, Ph.D. thesis, University of Western Australia (March 2001)
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science 1 (1975)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, N.D., Bohr, N. (2004). Termination Analysis of the Untyped λ-Calculus. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive