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 Lévy's family reductions. Starting from this consideration, we propose a new measure for what could be considered as "the intrinsic complexity" of λ-terms.