Efficient implementation of evaluation strategies via token-guided graph rewriting

Koko Muroya; Dan Ghica

Efficient implementation of evaluation strategies via token-guided graph rewriting

Koko Muroya, Dan Ghica

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

128 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)
Publisher	Open Publishing Association
Pages	52-66
Number of pages	15
Publication status	Published - 16 Feb 2018
Event	Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017) - Oxford, United Kingdom Duration: 8 Sept 2017 → 8 Sept 2017

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association
Volume	265
ISSN (Electronic)	2075-2180

Conference

Conference	Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)
Country/Territory	United Kingdom
City	Oxford
Period	8/09/17 → 8/09/17

Access to Document

EfficientImplementation
Accepted for publication on http://www.ki.informatik.uni-frankfurt.de/WPTE17/
Accepted author manuscript, 483 KBLicence: Creative Commons: Attribution (CC BY)

http://eptcs.web.cse.unsw.edu.au/content.cgi?WPTE2017Licence: Creative Commons: Attribution (CC BY)

Cite this

Muroya, K., & Ghica, D. (2018). Efficient implementation of evaluation strategies via token-guided graph rewriting. In Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017) (pp. 52-66). (Electronic Proceedings in Theoretical Computer Science; Vol. 265). Open Publishing Association. http://eptcs.web.cse.unsw.edu.au/content.cgi?WPTE2017

@inproceedings{b367c62a1a5d4f88b8b6294284230661,

title = "Efficient implementation of evaluation strategies via token-guided graph rewriting",

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 theintroduction of an abstract machine for call-by-need, inspired by Girard{\textquoteright}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 showsoundness 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{\textquoteright}s taxonomy of abstract machines.",

author = "Koko Muroya and Dan Ghica",

year = "2018",

month = feb,

day = "16",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "52--66",

booktitle = "Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)",

note = " Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017) ; Conference date: 08-09-2017 Through 08-09-2017",

}

Muroya, K & Ghica, D 2018, Efficient implementation of evaluation strategies via token-guided graph rewriting. in Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017). Electronic Proceedings in Theoretical Computer Science, vol. 265, Open Publishing Association, pp. 52-66, Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017), Oxford, United Kingdom, 8/09/17. <http://eptcs.web.cse.unsw.edu.au/content.cgi?WPTE2017>

Efficient implementation of evaluation strategies via token-guided graph rewriting. / Muroya, Koko; Ghica, Dan.
Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017). Open Publishing Association, 2018. p. 52-66 (Electronic Proceedings in Theoretical Computer Science; Vol. 265).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Efficient implementation of evaluation strategies via token-guided graph rewriting

AU - Muroya, Koko

AU - Ghica, Dan

PY - 2018/2/16

Y1 - 2018/2/16

N2 - 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 theintroduction 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 showsoundness 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.

AB - 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 theintroduction 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 showsoundness 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.

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 52

EP - 66

BT - Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)

PB - Open Publishing Association

T2 - Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE2017)

Y2 - 8 September 2017 through 8 September 2017

ER -

Efficient implementation of evaluation strategies via token-guided graph rewriting

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this