Abstract
Call-by-need (which is an equivalent but more efficient implementation of call-by-name for applicative languages) is quite expensive with current hardware and also does not permit full use of the tricks (such as memo functions and recursion removal) associated with the cheaper call-by-value. However the latter mechanism may fail to terminate for perfectly well-defined equations and also invalidates some program transformation schemata.
Here a method is developed which determines lower and upper bounds on the definedness of terms and functions, this being specialised to provide sufficient conditions to change the order and position of evaluation keeping within the restriction of strong equivalence. This technique is also specialised into an algorithm analogous to type-checking for practical use which can also be used to drive a program transformation package aimed at transforming call-by-need into call-by-value at ‘compile’ time.
We also note that many classical problems can be put in the framework of proving the strong equivalence where weak equivalence is easy to show (for example the Darlington/Burstall fold/unfold program transformation).
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Berry, G., Bottom-up computation of recursive programs, Research Report 133, IRIA-Laboria, 78150 Le Chesnay, France (1975).
Cousot, P. and Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proc. of Conference on Principles of Programming Languages, Los Angeles (1977).
Darlington, J. and Burstall, R.M., A transformation system for developing recursive programs, JACM, Vol. 24, No. 1 (1977).
Friedman, D.P. and Wise, D.S., CONS should not evaluate its arguments, Proc. of 3rd International Colloquium on Automata, Languages and Programming, Edinburgh (1976).
Gordon, M.J.C., Milner, A.J.R.G. and Wadsworth, C., Edinburgh LCF, Lecture Notes in Computer Science, Springer-Verlag (1979).
Gordon, M.J.C., Milner, A.J.R.G., Morris, L., Newey, M. and Wadsworth, C., A meta-language for interactive proof in LCF, Proc. of 5th ACM STGACT-SIGPLAN Conference on Principles of Programming Languages, Tucson, Arizona (1978).
Lang, B., Threshold evaluation and the semantics of call-by-value, assignment and generic procedures, Proc. of Conference on Principles of Programming Languages, Los Angeles (1977).
Schwarz, J., Using annotations to make recursion equations behave, DAI Research Report No. 43, Dept. of Artificial Intelligence, University of Edinburgh (1977). Also to appear in IEEE Transactions on Software Engineering.
Vuillemin, J., Proof techniques for recursive programs, Ph.D. thesis (chapter 2), published as a paper in 1974 as Correct and optimal implementations of recursion in a simple programming language, Journal of Computer and Systems Sciences, 9, 332–354 (1974).
Wadsworth, C., Semantics and pragmatics of the lambda calculus, Ph.D. thesis, Programming Research Group, Oxford University (1971).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1980 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mycroft, A. (1980). The theory and practice of transforming call-by-need into call-by-value. In: Robinet, B. (eds) International Symposium on Programming. Programming 1980. Lecture Notes in Computer Science, vol 83. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09981-6_19
Download citation
DOI: https://doi.org/10.1007/3-540-09981-6_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09981-9
Online ISBN: 978-3-540-39233-0
eBook Packages: Springer Book Archive