Koko Muroya ; Dan R. Ghica - The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter

lmcs:4340 - Logical Methods in Computer Science, October 30, 2019, Volume 15, Issue 4 - https://doi.org/10.23638/LMCS-15(4:7)2019
The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter

Authors: 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. 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 \emph{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.


    Volume: Volume 15, Issue 4
    Published on: October 30, 2019
    Accepted on: October 30, 2019
    Submitted on: March 2, 2018
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.fscd.2022.29
    • 10.4230/lipics.fscd.2022.29
    Rewriting for Monoidal Closed Categories
    Alvarez-Picallo, Mario ; Ghica, Dan ; Sprunger, David ; Zanasi, Fabio ;

    Share

    Consultation statistics

    This page has been seen 501 times.
    This article's PDF has been downloaded 278 times.