This note is about encoding Turing machines into the lambda-calculus.

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. 39 pages, 4 figures

We present an efficient implementation of the full-reducing call-by-value strategy for the pure λ-calculus in the form of an abstract machine. The presented machine has been systematically derived using Danvy et al.’s functional correspondence that connects higher-order interpreters with abstract-machine models by a well-established transformation technique. It improves on a previously presented machine by Biernacka et al. in terms of efficiency: the new machine simulates β-reduction with the overhead polynomial in the number of β-steps and in the size of the initial term. Thus, the machine makes a “reasonable” (in the sense of Accattoli et al.) implementation of Strong CbV.