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). © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Lago, U. D., & Martini, S. (2006). An invariant cost model for the lambda calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3988 LNCS, pp. 105–114). Springer Verlag. https://doi.org/10.1007/11780342_11
Mendeley helps you to discover research relevant for your work.