Abstract
We define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. That is, under the proposed cost model, Turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial time overhead. The model only relies on combinatorial properties of usual beta-reduction, without any reference to a specific machine or evaluator. In particular, the cost of a single beta reduction is proportional to the difference between the size of the redex and the size of the reduct. In this way, the total cost of normalizing a lambda term will take into account the size of all intermediate results (as well as the number of steps to normal form).
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.
Similar content being viewed by others
References
Asperti, A.: On the complexity of beta-reduction. In: Proc. 23rd ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 110–118 (1996)
Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol. 45. Cambridge University Press, Cambridge (1998)
Dal Lago, U., Hofmann, M.: Quantitative models and implicit complexity. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 189–200. Springer, Heidelberg (2005)
Dal Lago, U., Martini, S.: An invariant cost model for the lambda calculus (2005) (extended Version) Available at: http://arxiv.org/cs.LO/0511045
de Bruijn, N.G.: Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae 34(5), 381–392 (1972)
Dezani-Ciancaglini, M., della Rocca, S.R., Saitta, L.: Complexity of lambda-terms reductions. RAIRO Informatique Theorique 13(3), 257–287 (1979)
Frandsen, G.S., Sturtivant, C.: What is an efficient implementation of the lambda-calculus? In: Proc. 5th ACM Conference on Functional Programming Languages and Computer Architecture, pp. 289–312 (1991)
Lamping, J.: An algorithm for optimal lambda calculus reduction. In: Proc. 17th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 16–30 (1990)
Lawall, J.L., Mairson, H.G.: Optimality and inefficiency: What isn’t a cost model of the lambda calculus? In: Proc. 1996 ACM SIGPLAN International Conference on Functional Programming, pp. 92–101 (1996)
Lawall, J.L., Mairson, H.G.: On global dynamics of optimal graph reduction. In: Proc. 1997 ACM SIGPLAN International Conference on Functional Programming, pp. 188–195 (1997)
Lévy, J.-J.: Réductions corrected et optimales dans le lambda-calcul. Université Paris 7, Thèses d’Etat (1978)
Della Rocca, S.R., Paolini, L.: The parametric lambda-calculus. Texts in Theoretical Computer Science: An EATCS Series. Springer, Heidelberg (2004)
van Emde Boas, P.: Machine models and simulation. In: Handbook of Theoretical Computer Science. Algorithms and Complexity (A), vol. A, pp. 1–66. MIT Press, Cambridge (1990)
Wadsworth, C.: Some unusual λ-calculus numeral systems. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London (1980)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U., Martini, S. (2006). An Invariant Cost Model for the Lambda Calculus. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds) Logical Approaches to Computational Barriers. CiE 2006. Lecture Notes in Computer Science, vol 3988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780342_11
Download citation
DOI: https://doi.org/10.1007/11780342_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35466-6
Online ISBN: 978-3-540-35468-0
eBook Packages: Computer ScienceComputer Science (R0)