Document Open Access Logo

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

Authors Koko Muroya, Dan R. Ghica

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.32.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Author Details

Koko Muroya
Dan R. Ghica

Cite As Get BibTex

Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.32

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.

Subject Classification

Keywords
  • Geometry of Interaction
  • cost analysis
  • call-by-need reduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Beniamino Accattoli. The complexity of abstract machines. In WPTE 2016, volume 235 of EPTCS, pages 1-15, 2017. Google Scholar
  2. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In ICFP 2014, pages 363-376. ACM, 2014. Google Scholar
  3. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. Parallelism and synchronization in an infinitary context. In LICS 2015, pages 559-572. IEEE, 2015. Google Scholar
  4. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The Geometry of Parallelism: classical, probabilistic, and quantum effects. In POPL 2017, pages 833-845. ACM, 2017. Google Scholar
  5. Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. In LICS 2011, pages 133-142. IEEE Computer Society, 2011. Google Scholar
  6. Ugo Dal Lago and Barbara Petit. Linear dependent types in a call-by-value scenario. In PPDP 2012, pages 115-126. ACM, 2012. Google Scholar
  7. Ugo Dal Lago and Ulrich Schöpp. Computation by interaction for space-bounded functional programming. Inf. Comput., 248:150-194, 2016. Google Scholar
  8. Vincent Danos and Laurent Regnier. Local and asynchronous beta-reduction (an analysis of Girard’s execution formula). In LICS 1993, pages 296-306. IEEE Computer Society, 1993. Google Scholar
  9. Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal lambda-machines. Elect. Notes in Theor. Comp. Sci., 3:40-60, 1996. Google Scholar
  10. Olivier Danvy and Ian Zerny. A synthetic operational account of call-by-need evaluation. In PPDP 2013, pages 97-108. ACM, 2013. Google Scholar
  11. Maribel Fernández and Ian Mackie. Call-by-value lambda-graph rewriting without rewriting. In ICGT 2002, volume 2505 of LNCS, pages 75-89. Springer, 2002. Google Scholar
  12. Dan R. Ghica. Geometry of Synthesis: a structured approach to VLSI design. In POPL 2007, pages 363-375. ACM, 2007. Google Scholar
  13. Dan R. Ghica and Alex Smith. Geometry of Synthesis III: resource management through type inference. In POPL 2011, pages 345-356. ACM, 2011. Google Scholar
  14. Dan R. Ghica, Alex Smith, and Satnam Singh. Geometry of Synthesis IV: compiling affine recursion into static hardware. In ICFP, pages 221-233, 2011. Google Scholar
  15. Jean-Yves Girard. Linear logic. Theor. Comp. Sci., 50:1-102, 1987. Google Scholar
  16. Jean-Yves Girard. Geometry of Interaction I: interpretation of system F. In Logic Colloquium 1988, volume 127 of Studies in Logic &Found. Math., pages 221-260. Elsevier, 1989. Google Scholar
  17. Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. Memoryful Geometry of Interaction: from coalgebraic components to algebraic effects. In CSL-LICS 2014, pages 52:1-52:10. ACM, 2014. Google Scholar
  18. Ian Mackie. The Geometry of Interaction machine. In POPL 1995, pages 198-208. ACM, 1995. Google Scholar
  19. Robin Milner. Communication and concurrency. PHI Series in Computer Science. Prentice Hall, 1989. Google Scholar
  20. Koko Muroya and Dan R. Ghica. The dynamic geometry of interaction machine: A call-by-need graph rewriter. CoRR, arXiv:1703.10027, 2017. URL: https://arxiv.org/abs/1703.10027.
  21. Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo. Memoryful Geometry of Interaction II: recursion and adequacy. In POPL 2016, pages 748-760. ACM, 2016. Google Scholar
  22. Ulrich Schöpp. Computation-by-interaction with effects. In APLAS 2011, volume 7078 of Lect. Notes Comp. Sci., pages 305-321. Springer, 2011. Google Scholar
  23. Ulrich Schöpp. Call-by-value in a basic logic for interaction. In APLAS 2014, volume 8858 of Lect. Notes Comp. Sci., pages 428-448. Springer, 2014. Google Scholar
  24. Ulrich Schöpp. Organising low-level programs using higher types. In PPDP 2014, pages 199-210. ACM, 2014. Google Scholar
  25. François-Régis Sinot. Call-by-name and call-by-value as token-passing interaction nets. In TLCA 2005, volume 3461 of Lect. Notes Comp. Sci., pages 386-400. Springer, 2005. Google Scholar
  26. François-Régis Sinot. Call-by-need in token-passing nets. Math. Struct. in Comp. Sci., 16(4):639-666, 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact