On the complexity of beta-reduction

Abstract

We prove that the complexity of Lamping's optimal graph reduction technique for the λ-calculus can be exponential in the number of Levy's family reductions. Starting from this consideration, we propose a new measure for what could be considered as 'the intrinsic complexity' of λ-terms.