The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Colleges, School and Institutes


Girard’s Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been alsosuccessfully applied to programming languages. One way is to use abstract machines that pass a token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of
a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid
replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our
quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of abstract machines.


Original languageEnglish
Title of host publicationLIPIcs: Leibniz International Proceedings in Informatics
Subtitle of host publicationProceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
EditorsValentin Goranko, Mads Dam
Publication statusPublished - 1 Aug 2017
Event26th EACSL Annual Conference on Computer Science Logic (CSL 2017) - Stockholm, Sweden
Duration: 20 Aug 201724 Aug 2017


Conference26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Abbreviated titleCSL 2017
Internet address


  • geometry of interaction , cost analysis , call-by-need reduction