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).
An invariant cost model for the lambda calculus / DAL LAGO, Ugo; Martini, Simone. - STAMPA. - LNCS 3988:(2006), pp. 105-114. (Intervento presentato al convegno Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006 tenutosi a Swansea, UK nel 30 June - 5 July, 2006).
An invariant cost model for the lambda calculus
DAL LAGO, UGO;MARTINI, SIMONE
2006
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).I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
