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

Koko Muroya, Dan R. Ghica

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)
96 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. 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.
Original languageEnglish
Article number4340
Number of pages32
JournalLogical Methods in Computer Science
Volume15
Issue number4
DOIs
Publication statusPublished - 30 Oct 2019

Keywords

  • Geometry of Interaction
  • cost analysis
  • evaluation strategies

Fingerprint

Dive into the research topics of 'The dynamic geometry of interaction machine: a token-guided graph rewriter'. Together they form a unique fingerprint.

Cite this