Skip to Main content Skip to Navigation
New interface
Journal articles

(Leftmost-outermost) beta reduction is invariant, indeed

Beniamino Accattoli 1, 2 Ugo Dal Lago 3, 4 
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
4 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomial overhead in time. Is λ-calculus a reasonable machine? Is there a way to measure the computational complexity of a λ-term? This paper presents the first complete positive answer to this long-standing problem. Moreover , our answer is completely machine-independent and based on a standard notion in the theory of λ-calculus: the length of a leftmost-outermost derivation to normal form is an invariant , i.e. reasonable, cost model. Such a theorem cannot be proved by directly relating λ-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 large 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 the LSC is invariant with respect to the λ-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 λ-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction , called useful. Useful evaluation produces a compact, shared representation of the normal form, by avoiding those steps that only unshare the output without contributing to β-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.
Document type :
Journal articles
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Ugo Dal Lago Connect in order to contact the contributor
Submitted on : Monday, June 27, 2016 - 2:48:27 PM
Last modification on : Friday, July 8, 2022 - 10:09:34 AM


Publisher files allowed on an open archive



Beniamino Accattoli, Ugo Dal Lago. (Leftmost-outermost) beta reduction is invariant, indeed. Logical Methods in Computer Science, 2016, ⟨10.2168/LMCS-12(1:4)2016⟩. ⟨hal-01337712⟩



Record views


Files downloads