The weak lambda calculus as a reasonable machine

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). Key words: Lambda calculus, Computational complexity, Invariance thesis, Cost model

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Ugo Dal Lago, Simone Martini
• Keywords: Cost Model, Invariance Thesis, Single Beta Reduction, TCS 2008, Theoretical Computer Science