Hostname: page-component-cd9895bd7-hc48f Total loading time: 0 Render date: 2024-12-23T18:17:34.241Z Has data issue: false hasContentIssue false
  • English
  • Français

Abstract machines, optimal reduction, and streams

Published online by Cambridge University Press:  08 April 2019

Anna Chiara Lai ,
Marco Pedicini Open the ORCID record for Marco Pedicini [Opens in a new window]  and
Mario Piazza
Anna Chiara Lai
Affiliation:
Department of Basic and Applied Sciences for Engineering, Sapienza University of Rome, Via Antonio Scarpa 16, 00181 Rome, Italy
Marco Pedicini*
Affiliation:
Department of Mathematics and Physics, Roma Tre University, Via della Vasca Navale 84, 00146 Rome, Italy
Mario Piazza
Affiliation:
Classe di Lettere e Filosofia, Scuola Normale Superiore, Piazza dei Cavalieri 7, 56126 Pisa, Italy
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we propose and explore a new approach to abstract machines and optimal reduction via streams, infinite sequences of elements. We first define a sequential abstract machine capable of performing directed virtual reduction (DVR) and then we extend it to its parallel version, whose equivalence is explained through the properties of DVR itself. The result is a formal definition of the λ-calculus interpreter called Parallel Environment for Lambda Calculus Reduction (PELCR), a software for λ-calculus reduction based on the Geometry of Interaction. In particular, we describe PELCR as a stream-processing abstract machine, which in principle can also be applied to infinite streams.

Keywords

Geometry of InteractionParallel ImplementationFunctional ProgrammingStreamsLinear LogicCurry-Howard Isomorphism
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Issue 9 , October 2019 , pp. 1379 - 1410
Copyright
© Cambridge University Press 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Accattoli, B., Barenbaum, P. and Mazza, D. (2014). Distilling abstract machines. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1–3, 2014, 363–376.Google Scholar
Allombert, V. and Gava, F. (2018). An ML implementation of the MULTI-BSP model. In: 2018 International Conference on High Performance Computing Simulation (HPCS), 500–507. Orleans, France.CrossRefGoogle Scholar
Asperti, A. and Chroboczek, J. (1997). Safe operators: Brackets closed forever optimizing optimal lambda-calculus implementations. Applicable Algebra in Engineering, Communication and Computing 8(6) 437–468.CrossRefGoogle Scholar
Asperti, A., Giovanetti, C. and Naletto, A. (1996). The Bologna optimal higher-order machine. Journal of Functional Programming 6(6) 763–810.CrossRefGoogle Scholar
Asperti, A. and Guerrini, S. (1998). The Optimal Implementation of Functional Programming languages, vol. 45, Cambridge University Press.Google Scholar
Baillot, P. and Pedicini, M. (2001). Elementary complexity and geometry of interaction. Fund. Inform. 45(1–2) 1–31. Typed lambda calculi and applications (L’Aquila, 1999).Google Scholar
Canavese, D., Cesena, E., Ouchary, R., Pedicini, M. and Roversi, L. (2014). Can a light typing discipline be compatible with an efficient implementation of finite fields inversion? Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8552:38–57.Google Scholar
Canavese, D., Cesena, E., Ouchary, R., Pedicini, M. and Roversi, L. (2015). Light combinators for finite fields arithmetic. Science of Computer Programming 111(3) 365–394. Special Issue on Foundational and Practical Aspects of Resource Analysis (FOPARA) 2009–2011.CrossRefGoogle Scholar
Cesena, E., Pedicini, M. and Roversi, L. (2012). Typing a core binary-field arithmetic in a light logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7177 LNCS:19–35.Google Scholar
Charles, P., Grothoff, C., Saraswat, V., Donawa, C., Kielstra, A., Ebcioglu, K., von Praun, C. and Sarkar, V. (2005). X10: an object-oriented approach to non-uniform cluster computing. In: Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA ’05, 519–538. ACM. San Diego, California, USA.Google Scholar
Cousineau, G. and Mauny, M. (1998). The Functional Approach to Programming, Cambridge University Press.CrossRefGoogle Scholar
Curien, P.-L. (1991). An abstract framework for environment machines. Theoretical Computer Science 82(2) 389–402.CrossRefGoogle Scholar
Dal Lago, U., Faggian, C., Valiron, B. and Yoshimizu, A. (2015). Parallelism and synchronization in an infinitary context. In: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), IEEE Computer Society, Los Alamitos, CA, 559–572.CrossRefGoogle Scholar
Danos, V., Pedicini, M. and Regnier, L. (1997). Directed virtual reductions. In: Computer science logic (Utrecht, 1996), vol. 1258 of Lecture Notes in Computer Science Springer, Berlin, 76–88.CrossRefGoogle Scholar
Danos, V. and Regnier, L. (1993). Local and asynchronous beta-reduction (an analysis of Girard’s execution formula). In: Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993), IEEE Computer Society Press, 296–306.CrossRefGoogle Scholar
Danos, V. and Regnier, L. (1995). Proof-nets and the Hilbert space. In: Advances in Linear Logic, Montreal, Quebec, Canada. Cambridge University Press, 307–328.CrossRefGoogle Scholar
Fairbairn, J. and Wray, S. (1987). TIM : A Simple Lazy Abstract Machine to Execute Supercombinators. In: Kahn, G. (eds.) Proceedings of Conference on Functional Programming and Computer Architecture, vol. 274 of Lecture Notes in Computer Science, Springer-Verlag, 34–45.Google Scholar
Girard, J.-Y. (1989). Geometry of Interaction I. Interpretation of system F. In: Logic Colloquium ’88 (Padova, 1988), vol. 127 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 221–260.Google Scholar
Girard, J.-Y. (1990). Geometry of Interaction II. Deadlock-free algorithms. In: COLOG-88 (Tallinn, 1988), volume 417 of Lecture Notes in Computer Science, Springer, Berlin, 76–93.CrossRefGoogle Scholar
Girard, J.-Y. (1995). Geometry of interaction III: Accommodating the additives. In Advances in Linear Logic, Cambridge University Press, 329–389.CrossRefGoogle Scholar
Gonthier, G., Abadi, M. and Lévy, J.-J. (1992). The Geometry of Optimal Lambda Reduction. In: Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, 15–26.Google Scholar
Hindley, J. R. and Seldin, J. P. (1986). Introduction to Combinators and λ-Calculus, vol. 1 of London Mathematical Society Student Texts, Cambridge University Press.Google Scholar
Lamping, J. (1989). An algorithm for optimal lambda calculus reduction. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 16–30. San Francisco, California, USA.Google Scholar
Landin, P. J. (1964). The mechanical evaluation of expressions. Computer Journal 6(4) 308–320.CrossRefGoogle Scholar
Lawson, M. V. (1998). Inverse Semigroups: The Theory of Partial Symmetries, World Scientific.CrossRefGoogle Scholar
Lévy, J.-J. (1978). Réductions Correctes et Optimales Dans le Lambda-Calcul. PhD thesis, Université Paris VII.Google Scholar
Lévy, J.-J. (1980). Optimal reductions in the lambda-calculus. To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 159–191.Google Scholar
Mackie, I. (1995). The geometry of interaction machine. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 198–208. San Francisco, California, USA.Google Scholar
Muroya, K. and Ghica, D. R. (2017). The dynamic geometry of interaction machine: a call-by-need graph rewriter. In: Computer science logic 2017, volume 82 of LIPIcs. Leibniz Int. Proc. Inform., Art. No. 32, 15. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern.Google Scholar
Pedicini, M. (1998). Exécution et Programmes. PhD thesis, Université Paris VII.Google Scholar
Pedicini, M., Pellitta, G. and Piazza, M. (2014). Sequential and parallel abstract machines for optimal reduction. In: Hage, J. (ed.) Preproceedings of the 15th Symposium on Trends in. Functional Programming. Soesterberg, the Netherlands.Google Scholar
Pedicini, M. and Piazza, M. (2018). Kálmar elementary complexity and von Neumann algebras. Panamerican Mathematical Journal 28(4) 1–28.Google Scholar
Pedicini, M. and Quaglia, F. (2000). A parallel implementation for optimal lambda-calculus reduction. In: Proceedings of the 2nd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming – PPDP ’00. Montreal, Quebec, Canada.Google Scholar
Pedicini, M. and Quaglia, F. (2002). Scheduling vs communication in PELCR. In: Monien, B. and Feldmann, R. (eds.) Euro-Par 2002 Parallel Processing, Springer, Berlin Heidelberg, 648–655.CrossRefGoogle Scholar
Pedicini, M. and Quaglia, F. (2007). PELCR: parallel environment for optimal lambda-calculus reduction. ACM Transactions on Computational Logic (TOCL) 8(3).CrossRefGoogle Scholar
Pinto, J. S. (2001). Parallel Implementation Models for the Lambda-Calculus Using the Geometry of Interaction. In: Abramsky, S. (eds.) Typed Lambda Calculi and Applications, vol. 2044 of Lecture Notes in Computer Science, Springer, Berlin, 385–399.CrossRefGoogle Scholar
Regnier, L. (1992). Lambda-calcul et réseaux. PhD thesis, Université Paris VII.Google Scholar
Rutten, J. J. M. M. (2005a). A coinductive calculus of streams. Mathematical Structures in Computer Science 15(01) 93–147.CrossRefGoogle Scholar
Rutten, J. J. M. M. (2005b). A tutorial on coinductive stream calculus and signal flow graphs. Theoretical Computer Science 343(3) 443–481.CrossRefGoogle Scholar
Solieri, M. (2016). Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: A minimalist approach. Mathematical Structures in Computer Science 1–43.Google Scholar
Valiant, L. G. (1990). A bridging model for parallel computation. Communications of the Association of Computing Machinery 33(8) 103–111.CrossRefGoogle Scholar
Valiant, L. G. (2011). A bridging model for multi-core computing. Journal of Computer and System Sciences 77(1) 154–166.CrossRefGoogle Scholar