Abstract machines, optimal reduction, and streams
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.