The dynamic geometry of interaction machine: a token-guided graph rewriter
Research output: Contribution to journal › Article
Colleges, School and Institutes
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.
|Number of pages||32|
|Journal||Logical Methods in Computer Science|
|Publication status||Published - 30 Oct 2019|
- Geometry of Interaction, cost analysis, evaluation strategies