The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
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-reductions and the size of the largest term in a computation -- as reasonable measures with respect to the invariance thesis of Slot...
Main Authors: | , , |
---|---|
Format: | Report |
Language: | unknown |
Published: |
arXiv
2019
|
Subjects: | |
Online Access: | https://dx.doi.org/10.48550/arxiv.1902.07515 https://arxiv.org/abs/1902.07515 |
id |
ftdatacite:10.48550/arxiv.1902.07515 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.48550/arxiv.1902.07515 2023-05-15T18:32:45+02:00 The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space Forster, Yannick Kunze, Fabian Roth, Marc 2019 https://dx.doi.org/10.48550/arxiv.1902.07515 https://arxiv.org/abs/1902.07515 unknown arXiv Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 CC-BY Computational Complexity cs.CC Logic in Computer Science cs.LO Programming Languages cs.PL FOS Computer and information sciences Preprint Article article CreativeWork 2019 ftdatacite https://doi.org/10.48550/arxiv.1902.07515 2022-04-01T08:48:13Z 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-reductions 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 [STOC~84]. 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 that terminate in (encodings) of 'true' or 'false'. We consider this result as a solution to the long-standing open problem, explicitly posed by Accattoli [ENTCS~18], of whether the natural measures for time and space of the $λ$-calculus are reasonable, at least in case of weak call-by-value evaluation. Our proof 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 n$, 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. Report The Pointers DataCite Metadata Store (German National Library of Science and Technology) |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
unknown |
topic |
Computational Complexity cs.CC Logic in Computer Science cs.LO Programming Languages cs.PL FOS Computer and information sciences |
spellingShingle |
Computational Complexity cs.CC Logic in Computer Science cs.LO Programming Languages cs.PL FOS Computer and information sciences Forster, Yannick Kunze, Fabian Roth, Marc The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space |
topic_facet |
Computational Complexity cs.CC Logic in Computer Science cs.LO Programming Languages cs.PL FOS Computer and information sciences |
description |
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-reductions 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 [STOC~84]. 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 that terminate in (encodings) of 'true' or 'false'. We consider this result as a solution to the long-standing open problem, explicitly posed by Accattoli [ENTCS~18], of whether the natural measures for time and space of the $λ$-calculus are reasonable, at least in case of weak call-by-value evaluation. Our proof 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 n$, 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. |
format |
Report |
author |
Forster, Yannick Kunze, Fabian Roth, Marc |
author_facet |
Forster, Yannick Kunze, Fabian Roth, Marc |
author_sort |
Forster, Yannick |
title |
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space |
title_short |
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space |
title_full |
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space |
title_fullStr |
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space |
title_full_unstemmed |
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space |
title_sort |
weak call-by-value λ-calculus is reasonable for both time and space |
publisher |
arXiv |
publishDate |
2019 |
url |
https://dx.doi.org/10.48550/arxiv.1902.07515 https://arxiv.org/abs/1902.07515 |
genre |
The Pointers |
genre_facet |
The Pointers |
op_rights |
Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 |
op_rightsnorm |
CC-BY |
op_doi |
https://doi.org/10.48550/arxiv.1902.07515 |
_version_ |
1766216932769398784 |