Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
An Invariant Cost Model for the Lambda Calculus

Speaker: Ugo Dal Lago
Author(s): Ugo Dal Lago and Simone Martini
Slot: Array, 11:30-11:50, col. 2


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

websites: Arnold Beckmann 2006-06-09