Efficient implementation of evaluation strategies via token-guided graph rewriting

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Colleges, School and Institutes

Abstract

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.

Details

Original languageEnglish
Title of host publicationProceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)
Publication statusPublished - 16 Feb 2018
Event Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017) - Oxford, United Kingdom
Duration: 8 Sep 20178 Sep 2017

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume265
ISSN (Electronic)2075-2180

Conference

Conference Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)
CountryUnited Kingdom
CityOxford
Period8/09/178/09/17