Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Małgorzata Biernacka, Witold Charatonik, Tomasz Drab

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.

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

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.
Paper Structure (22 sections, 18 theorems, 29 equations, 4 figures, 9 tables)

This paper contains 22 sections, 18 theorems, 29 equations, 4 figures, 9 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Reduction semantics in the lambda calculus
  4. The call-by-need strategy
  5. Higher-order normalizers
  6. Normal-order normalizer
  7. An optimized, call-by-need normalizer
  8. Derivation of an abstract machine
  9. The abstract machine
  10. Elaborate example execution
  11. Empirical execution lengths
  12. Properties of the machine
  13. Decoding
  14. Alternative decodings
  15. Ghost abstract machine for RKNL
  16. ...and 7 more sections

Key Result

Lemma 5.1

${\underline{{\langle {{( t, [\,] )}}, {[\,]}, {[\,]}\rangle_{\textcolor{blue}{\triangledown}}}}_{\,\mathsf{k}}} =_\alpha t$.

Figures (4)

  • Figure 1: Automata for the grammars of contexts
  • Figure 2: Plot of potentials of configurations and stores for the execution of term ${{{({{\lambda{x}. {{{{{{{c}\,{x}}}}\,{x}}}}}})}\,{({{{({{\lambda{y}. {{{\lambda{z}. {{{{I}\,{z}}}}}}}}})}\,{\Omega}}})}}}$ as presented in Table \ref{['fig:execution_ex_ref']}.
  • Figure 3: Plot of potentials for ${{{{c_6}\,{\mathit{dub}}}}\,{({\lambda{x}. {{{I}\,{x}}}})}}$
  • Figure 4: Plot of potentials for initial configurations of the evaluation of the term $\Omega$

Theorems & Definitions (37)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Example 2.4
  • Example 2.5
  • Example 2.6
  • Remark 1
  • Remark 2
  • Lemma 5.1: load correctness
  • proof
  • ...and 27 more