English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We study the weak call-by-value $\lambda$-calculus as a model forcomputational complexity theory and establish the natural measures for time andspace -- the number of beta-reductions and the size of the largest term in acomputation -- as reasonable measures with respect to the invariance thesis ofSlot and van Emde Boas [STOC~84]. More precisely, we show that, using thosemeasures, Turing machines and the weak call-by-value $\lambda$-calculus cansimulate each other within a polynomial overhead in time and a constant factoroverhead in space for all computations that terminate in (encodings) of 'true'or 'false'. We consider this result as a solution to the long-standing openproblem, explicitly posed by Accattoli [ENTCS~18], of whether the naturalmeasures for time and space of the $\lambda$-calculus are reasonable, at leastin case of weak call-by-value evaluation.  Our proof relies on a hybrid of two simulation strategies of reductions inthe weak call-by-value $\lambda$-calculus by Turing machines, both of which areinsufficient if taken alone. The first strategy is the most naive one in thesense that a reduction sequence is simulated precisely as given by thereduction rules; in particular, all substitutions are executed immediately.This simulation runs within a constant overhead in space, but the overhead intime might be exponential. The second strategy is heap-based and relies onstructure sharing, similar to existing compilers of eager functional languages.This strategy only has a polynomial overhead in time, but the space consumptionmight require an additional factor of $\log n$, which is essentially due to thesize of the pointers required for this strategy. Our main contribution is theconstruction and verification of a space-aware interleaving of the twostrategies, which is shown to yield both a constant overhead in space and apolynomial overhead in time.

The Weak Call-By-Value {\lambda}-Calculus is Reasonable for Both Time and Space