Higher-order Virtual Machine 3: uma reconstrução racional

Abstract

Higher-order Virtual Machine 3 (HVM3) is a compiler that generates high-performance code based on interaction nets. It stands out for its potential for massively parallel execution in its strict version and for the optimal reduction of λ-calculus terms in its lazy version. Despite its promising properties, its operational complexity and the lack of educational documentation represent a barrier for new researchers and developers. This work aims to fill this gap by providing an incremental and detailed description of the syntax, semantics, and inner workings of HVM3, with a focus on its Lazy version. Starting from the theoretical foundations of λ-calculus and interaction combinators, the virtual machine is reconstructed step-by-step through a series of sub-machines, each adding new features to the previous one. The process begins with the memory model, evolving into the implementation of interaction combinators, and subsequently incorporating arithmetic operations, references, pattern matching for Algebraic Data Types (ADTs), reduction prioritization mechanisms, and more. The result is a documentation that serves as a guide for understanding HVM3, making this powerful computational model more accessible and fostering future research in the field.