弱按值调用λ-演算在时间和空间上都是合理的
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
摘要：
我们研究了弱按值调用$λ$ -演算作为计算复杂性理论的模型，并建立了时间和空间的自然测度-β-约简的数量和计算中最大项的大小-作为Slot和van Emde Boas [STOC~84]的不变性命题的合理测度。更确切地说，我们表明，使用这些措施，图灵机和弱调用的值$λ$ -演算可以模拟对方在一个多项式开销的时间和一个常数因子开销的空间中的所有计算终止（编码）的“真”或“假”。我们认为这一结果是对长期存在的公开问题的解决方案，该问题由Accattoli [ENTCS~18]明确提出，即$λ$ -演算的时间和空间的自然度量是否合理，至少在弱按值调用评估的情况下。我们的证明依赖于一个混合的两个模拟策略的减少在弱呼叫按值$λ$ -演算的图灵机，这两个都是不够的，如果单独采取。第一个策略是最简单的一个，因为约简序列是按照约简规则精确模拟的;特别是，所有的替换都是立即执行的。这个模拟在空间上的开销是恒定的，但是时间上的开销可能是指数级的。第二种策略是基于堆的，依赖于结构共享，类似于现有的渴望函数式语言的编译器。该策略在时间上仅具有多项式开销，但是空间消耗可能需要额外的因子$\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-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
