Beta reduction is invariant, indeed

DOI10.1145/2603088.2603105zbMATH Open1394.03020arXiv1405.3311OpenAlexW2010239186MaRDI QIDQ4635589FDOQ4635589

Ugo Dal Lago, Beniamino Accattoli

Publication date: 23 April 2018

Published in: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

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 modelled after linear logic and 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 $$-redexes, i.e., the steps that cause the blow-up in size.

Full work available at URL: https://arxiv.org/abs/1405.3311

zbMATH Keywords

computational complexity\(\lambda\)-calculussharingcost modelsexplicit substitutions

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (11)

• Title not available (Why is that?)
• On abstract normalisation beyond neededness
• A Fresh Look at the λ-Calculus
• Proof nets and the call-by-value \(\lambda\)-calculus
• Processes, systems \& tests: defining contextual equivalences
• Title not available (Why is that?)
• On the value of variables
• On sharing, memoization, and polynomial time
• Parallel beta reduction is not elementary recursive
• Processes against tests: on defining contextual equivalences
• Polynomial time over the reals with parsimony

This page was built for publication: Beta reduction is invariant, indeed

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635589)