10.2168/LMCS-12(1:4)2016
https://lmcs.episciences.org/1627
Accattoli, Beniamino
Beniamino
Accattoli
Lago, Ugo Dal
Ugo Dal
Lago
0000-0001-9200-070X
(Leftmost-Outermost) Beta Reduction is Invariant, Indeed
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.
Comment: arXiv admin note: substantial text overlap with arXiv:1405.3311
episciences.org
Computer Science - Programming Languages
Computer Science - Logic in Computer Science
arXiv.org - Non-exclusive license to distribute
2023-03-23
2016-03-09
2016-03-09
eng
journal article
arXiv:1601.01233
10.48550/arXiv.1601.01233
1860-5974
10.4230/lipics.itp.2021.19
https://lmcs.episciences.org/1627/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 12, Issue 1
Researchers
Students