A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine

TL;DR

This paper presents RKNL, an abstract machine that efficiently implements strong call-by-need evaluation, achieving simplicity and bilinear overhead by deriving it from a higher-order evaluator using memothunks.

Contribution

The paper introduces RKNL, a novel abstract machine for strong call-by-need that is simple, efficient, and derived automatically from a higher-order evaluator.

Findings

RKNL extends the lazy Krivine machine conservatively.

RKNL simulates normal-order evaluation with bilinear step complexity.

The machine achieves linear overhead relative to beta-reductions and input size.

Abstract

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.