Strong call-by-need combines full normalization with the sharing discipline of lazy evaluation, yet no prior implementation achieved both simplicity and efficiency. We introduce RKNL, an abstract machine that realizes strong call-by-need with bilinear overhead. The machine has been derived automatically from a higher-order evaluator that uses the technique of memothunks to implement laziness. By employing an off-the-shelf transformation tool implementing the ``functional correspondence'' between higher-order interpreters and abstract machines, we obtained 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 a bilinear number of steps, i.e., linear in both the number of beta-reductions and the size of the input term.

翻译：强按需调用将完全规范化与惰性求值的共享规范相结合，但先前实现均未能同时兼顾简单性与高效性。我们提出RKNL抽象机，该机器能以双线性开销实现强按需调用。该机器基于采用记忆thunk技术实现惰性的高阶求值器，通过自动化推导生成。借助实现高阶解释器与抽象机之间“函数对应关系”的现成转换工具，我们获得了简洁的机器描述。证明表明，该机器保守扩展了用于弱按需调用策略的惰性Krivine机器版本，且能以双线性步数模拟正规序策略——即在β-规约次数与输入项规模上均呈线性关系。