License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.32
URN: urn:nbn:de:0030-drops-76886
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7688/
Go to the corresponding LIPIcs Volume Portal

Muroya, Koko ; Ghica, Dan R.

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

pdf-format:
LIPIcs-CSL-2017-32.pdf (0.6 MB)

Abstract

Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully 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.

BibTeX - Entry

@InProceedings{muroya_et_al:LIPIcs:2017:7688,
  author =	{Koko Muroya and Dan R. Ghica},
  title =	{{The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Valentin Goranko and Mads Dam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7688},
  URN =		{urn:nbn:de:0030-drops-76886},
  doi =		{10.4230/LIPIcs.CSL.2017.32},
  annote =	{Keywords: Geometry of Interaction, cost analysis, call-by-need reduction}
}

Keywords: Geometry of Interaction, cost analysis, call-by-need reduction
Collection: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 16.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI