一句话：从 memothunk 求值器自动推导强按需调用抽象机，证明其保守扩展 Krivine 机并以双线性步模拟 normal order。
强按需调用（strong call-by-need）要求在 lambda 演算的抽象体之下继续归约，是实现惰性函数式语言中规范化求值的关键，但其高效实现通常较为复杂。本文从使用 memothunks 实现惰性的高阶求值器出发，借助实现“函数式对应”（functional correspondence）的现成变换工具，自动推导出对应的抽象机，从而得到简洁且易理解的机器描述。作者进一步证明：所得机器保守扩展了弱按需调用策略下的惰性 Krivine 机，并且以双线性（bilinear）步数模拟 normal-order 策略。这一结果既保证了机器相对于经典弱求值器的兼容性，也给出了其归约效率的理论刻画。
We present an abstract machine for a strong call-by-need strategy in the lambda calculus. The machine has been derived automatically from a higher-order evaluator that uses the technique of memothunks to implement laziness. The derivation has been done with the use of an off-the-shelf transformation tool implementing the "functional correspondence" between higher-order interpreters and abstract machines, and it yields a simple and concise description of the machine. We prove that the resulting machine conservatively extends the lazy version of Krivine machine for the weak call-by-need strategy, and that it simulates the normal-order strategy in bilinear number of steps.
@article{paperbot1482,
title = {A simple and efficient implementation of strong call by need by an abstract machine},
author = {Małgorzata Biernacka and Witold Charatonik and Tomasz Drab},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3549822}
}