Efficient Implementation of Evaluation Strategies via Token-Guided Graph Rewriting

Koko Muroya
Dan R. Ghica

In implementing evaluation strategies of the lambda-calculus, both correctness and efficiency of implementation are valid concerns. While the notion of correctness is determined by the evaluation strategy, regarding efficiency there is a larger design space that can be explored, in particular the trade-off between space versus time efficiency. We contributed to the study of this trade-off by the introduction of an abstract machine for call-by-need, inspired by Girard's Geometry of Interaction, a machine combining token passing and graph rewriting. This work presents an extension of the machine, to additionally accommodate left-to-right and right-to-left call-by-value strategies. We show soundness and completeness of the extended machine with respect to each of the call-by-need and two call-by-value strategies. Analysing time cost of its execution classifies the machine as "efficient" in Accattoli's taxonomy of abstract machines.

In Horatiu Cirstea and David Sabel: Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), Oxford, UK, 8th September 2017, Electronic Proceedings in Theoretical Computer Science 265, pp. 52–66.
Published: 16th February 2018.

ArXived at: https://dx.doi.org/10.4204/EPTCS.265.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org