Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-38175
Titel: The weak call-by-value λ-calculus is reasonable for both time and space
VerfasserIn: Forster, Yannick
Kunze, Fabian
Roth, Marc
Sprache: Englisch
Titel: Proceedings of the ACM on Programming Languages
Bandnummer: 4
Heft: POPL
Seiten: 1-23
Verlag/Plattform: Association for Computing Machinery
Erscheinungsjahr: 2020
Freie Schlagwörter: invariance thesis
lambda calculus
weak call-by-value reduction
time and space complexity
abstract machines
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Journalartikel / Zeitschriftenartikel
Abstract: We study the weak call-by-value 𝜆-calculus as a model for computational complexity theory and establish the natural measures for time and space Ð the number of beta-reduction steps and the size of the largest term in a computation Ð as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas from 1984. More precisely, we show that, using those measures, Turing machines and the weak call-by-value 𝜆-calculus can simulate each other within a polynomial overhead in time and a constant factor overhead in space for all computations terminating in (encodings of) łtruež or łfalsež. The simulation yields that standard complexity classes like 𝑃, NP, PSPACE, or EXP can be defined solely in terms of the 𝜆-calculus, but does not cover sublinear time or space. Note that our measures still have the well-known size explosion property, where the space measure of a computation can be exponentially bigger than its time measure. However, our result implies that this exponential gap disappears once complexity classes are considered instead of concrete computations. We consider this result a first step towards a solution for the long-standing open problem of whether the natural measures for time and space of the 𝜆-calculus are reasonable. Our proof for the weak call-by-value 𝜆-calculus is the first proof of reasonability (including both time and space) for a functional language based on natural measures and enables the formal verification of complexity-theoretic proofs concerning complexity classes, both on paper and in proof assistants. The proof idea relies on a hybrid of two simulation strategies of reductions in the weak call-by-value 𝜆-calculus by Turing machines, both of which are insufficient if taken alone. The first strategy is the most naive one in the sense that a reduction sequence is simulated precisely as given by the reduction rules; in particular, all substitutions are executed immediately. This simulation runs within a constant overhead in space, but the overhead in time might be exponential. The second strategy is heap-based and relies on structure sharing, similar to existing compilers of eager functional languages. This strategy only has a polynomial overhead in time, but the space consumption might require an additional factor of log𝑛, which is essentially due to the size of the pointers required for this strategy. Our main contribution is the construction and verification of a space-aware interleaving of the two strategies, which is shown to yield both a constant overhead in space and a polynomial overhead in time.
DOI der Erstveröffentlichung: 10.1145/3371095
URL der Erstveröffentlichung: https://dl.acm.org/doi/10.1145/3371095
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-381755
hdl:20.500.11880/34466
http://dx.doi.org/10.22028/D291-38175
ISSN: 2475-1421
Datum des Eintrags: 23-Nov-2022
Bezeichnung des in Beziehung stehenden Objekts: Supplemental Material
In Beziehung stehendes Objekt: https://dl.acm.org/action/downloadSupplement?doi=10.1145%2F3371095&file=a27-forster.webm
Fakultät: MI - Fakultät für Mathematik und Informatik
Fachrichtung: MI - Informatik
Professur: MI - Prof. Dr. Gert Smolka
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
3371095.pdf348,52 kBAdobe PDFÖffnen/Anzeigen


Diese Ressource wurde unter folgender Copyright-Bestimmung veröffentlicht: Lizenz von Creative Commons Creative Commons