(Leftmost-Outermost) Beta Reduction is Invariant, Indeed

Abstract

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of lambda-calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating lambda-calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modeled after linear logic proof nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the lambda-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the lambda-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those steps that only unshare the output without contributing to beta-redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reductions and the thorough analysis of their properties.

arXiv admin note: substantial text overlap with arXiv:1405.3311

References in corpus (1)

• Beta Reduction is Invariant, Indeed (Long Version)

Cited by in corpus (11)

• The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Strong Call by Value is Reasonable for Time
• Positive Focusing is Directly Useful
• Semantic Bounds and Strong Call-by-Value Normalization
• Efficient Implementation of Evaluation Strategies via Token-Guided Graph Rewriting
• The (In)Efficiency of Interaction
• Hashing Modulo Context-Sensitive $\alpha$-Equivalence
• Linear Depth Increase of Lambda Terms along Leftmost-Outermost Beta-Reduction
• The Space of Interaction (long version)
• On the enumeration of closures and environments with an application to random generation