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.

Abstract machines, optimal reduction, and streams

Mario Piazza;
2019

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.
2019
Settore M-FIL/02 - Logica e Filosofia della Scienza
Settore INF/01 - Informatica
Geometry of the interaction Parallel Implementation Functional Programming Streams Linear Logic Curry-Howard Isomorphism
File in questo prodotto:
File Dimensione Formato  
abstract_machines_optimal_reduction_and_streams.pdf

accesso aperto

Tipologia: Published version
Licenza: Creative Commons
Dimensione 1.52 MB
Formato Adobe PDF
1.52 MB Adobe PDF

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11384/78344
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact