# The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter

arXiv: https://arxiv.org/abs/1803.00427 · HTML: https://mlsanity.com/paper/1803.00427/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Feb 2018.

## Built on by (most cited first, 1 of 1)

- [Functorial String Diagrams for Reverse-Mode Automatic Differentiation](https://mlsanity.com/paper/2107.13433/) (2021)

## Abstract (arXiv)

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.