Abstract
Termination analysis is genuinely useful for enabling optimisation in state-of-the-art compilers for lazy functional languages. Termination analysis techniques are typically restricted to determining termination in evaluation to weak head normal form; our projection-based technique gives much more detailed information, such as the fact that evaluation of an entire list or the entire spine of a list is certain to terminate, and hence gives the potential for much better compile-time optimisation.
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
S. Abramsky and C. Hankin. An introduction to abstract interpretation. Chapter 1 of Abstract Interpretation of Declarative Languages. S. Abramsky and C. Hankin, eds. Ellis-Horwood, 1987.
P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation (preliminary draft). LIX, Ecole Polytechnique, 91128 Palaiseau Cedex, France, May 15, 1991.
K. Davis. Higher-order Binding-time Analysis. Proceedings of the 1993 ACM on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’ 93).
K. Davis and P. Wadler. Strictness analysis in 4D. Functional Programming: Proceedings of the 1990 Glasgow Workshop, 13-15 August 1990, Ullapool, Scotland. Simon L. Peyton Jones et al., eds. Springer Workshops in Computing. Springer-Verlag, 1991.
K. Davis and P. Wadler. Strictness analysis: Proved and improved. Functional Programming: Proceedings of the 1989 Glasgow Workshop, 21-23 August 1989, Fraserburgh, Scotland. K. Davis and J. Hughes, eds. Springer Workshops in Computing. Springer-Verlag, 1990.
A. Ferguson. Concrete Data Structures. Functional Programming: Proceedings of the 1992 Glasgow Workshop, 6-8 July 1992, Ayr, Scotland. Springer Workshops in Computing, Springer-Verlag, 1992.
P.H. Hartel. On the benefits of different analyses in the compilation of lazy functional languages. 3rd Informal International Workshop on the Parallel Implementation of Functional Languages, Southampton, 1991.
R.J.M. Hughes and J. Launchbury. Projections for polymorphic first-order strictness analysis. Math. Struct, in Comp. Science, vol. 2, pp. 301–326, CUP, 1992.
S. Hunt. Frontiers and open sets in abstract interpretation. Functional Programming and Computer Architecture. (Imperial College, London, September 1989.) ACM, Addison-Wesley Publishing, Reading, MA, U.S.A. 1989.
J. Launchbury. Projection Factorisations in Partial Evaluation. Ph.D. Thesis, Glasgow University, Nov 89. Distinguished Dissertation in Computer Science, Vol 1, CUP, 1991.
A. Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. thesis, University of Edinburgh, 1981.
J. Seward. Solving recursive domain equations by term rewriting. Functional Programming: Proceedings of the 1993 Glasgow Workshop, 5-7 July 1993, Ayr, Scotland. Springer Workshops in Computing. Springer-Verlag, 1994 (this volume).
P. Wadler and J. Hughes. Projections for Strictness Analysis. Proceedings of Functional Programming Languages and Computer Architecture. LNCS 274. Springer-Verlag, 1987.
J. Young. The Theory and Practice of Semantic Program Analysis for Higher-Order Functional Programming Languages, Ph.D. thesis, Research report YALEU/DCS/RR-669, Yale University, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this chapter
Cite this chapter
Davis, K. (1994). Projection-based Termination Analysis. In: O’Donnell, J.T., Hammond, K. (eds) Functional Programming, Glasgow 1993. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3236-3_3
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3236-3_3
Publisher Name: Springer, London
Print ISBN: 978-3-540-19879-6
Online ISBN: 978-1-4471-3236-3
eBook Packages: Springer Book Archive