The dynamic geometry of interaction machine: a token-guided graph rewriter

Research output: Contribution to journalArticle

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. Aiming at a unified framework that would enable the study of this trade-off, we introduce an abstract machine, inspired by Girard's Geometry of Interaction (GoI), a machine combining token passing and graph rewriting. We show soundness and completeness of our abstract machine, called the Dynamic GoI Machine (DGoIM), with respect to three evaluations: call-by-need, left-to-right call-by-value, and right-to-left call-by-value. Analysing time cost of its execution classifies the machine as "efficient" in Accattoli's taxonomy of abstract machines.

Bibliographic note

Logical Methods in Computer Science Special Issue for the Confernece on Computer Science Logic (CSL) 2017

Details

Original languageEnglish
Article number4340
Number of pages32
JournalLogical Methods in Computer Science
Publication statusAccepted/In press - 30 Jul 2019

Keywords

  • Geometry of Interaction, cost analysis, evaluation strategies