一句话：证明弱按值调用 λ-演算的 β-归约步数与最大项大小是合理的时间、空间度量，可与图灵机多项式时间、常数空间互模拟。
本文研究弱按值调用 λ-演算作为计算复杂度理论模型的合理性：其自然度量——β-归约步数（时间）与计算中最大项大小（空间）——是否满足 Slot 与 van Emde Boas 的不变性论题。作者证明，对终止于 true/false 编码的计算，图灵机与弱按值调用 λ-演算能以多项式时间开销和常数空间开销相互模拟，从而 P、NP、PSPACE、EXP 等复杂度类可仅用 λ-演算定义，但不覆盖次线性时间或空间。方法上，论文交织两种模拟：朴素立即替换模拟有常数空间但时间可能指数爆炸；基于堆的结构共享模拟有多项式时间但需额外 log n 空间。作者构造并验证空间感知的交织策略，同时获得常数空间与多项式时间开销。
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 P , 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 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.
@article{paperbot531,
title = {The weak call-by-value λ-calculus is reasonable for both time and space},
author = {Yannick Forster and Fabian Kunze and Marc Roth},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371095}
}