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

DOI10.4230/LIPICS.CSL.2017.32zbMATH Open1440.68044arXiv1703.10027OpenAlexW2962792150MaRDI QIDQ5111200FDOQ5111200

Dan R. Ghica, Koko Muroya

Publication date: 26 May 2020

Abstract: Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming language semantics. One way is to use abstract machines that pass a token on 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.

Full work available at URL: https://arxiv.org/abs/1703.10027

Recommendations

• The dynamic geometry of interaction machine: a token-guided graph rewriter
• In-place graph rewriting with interaction nets
• Graph Transformation with Dependencies for the Specification of Interactive Systems
• Computer Science Logic
• Towards a typed geometry of interaction
• scientific article; zbMATH DE number 2090088
• Confluence of graph rewriting with interfaces
• Theoretical Computer Science
• Graph transformation units with interleaving semantics

zbMATH Keywords

geometry of interactioncost analysiscall-by-need reduction

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Cited In (5)

• Title not available (Why is that?)
• A Fresh Look at the λ-Calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111200)