The Complexity of Abstract Machines
The lambda calculus is a peculiar computational model whose definition does not come with a notion of machine. Unsurprisingly, implementations of the lambda calculus have been studied for decades.
Abstract machines are implementations schema for fixed evaluation strategies that are a compromise between theory and practice: they are concrete enough to provide a notion of machine and abstract enough to avoid the many intricacies of actual implementations.
There is an extensive literature about abstract machines for the lambda-calculus, and yet — quite mysteriously — the efficiency of these machines with respect to the strategy that they implement has almost never been studied.
In this talk I will provide an unusual introduction to abstract machines, based on the complexity of their overhead with respect to the length of the implemented strategies. I will compare different approaches, optimizations, and evaluation strategies, providing a new modular and uniform perspective on abstract machines.
The results I will discuss are based on a series of recent works in collaboration with Pablo Barenbaum, Ugo Dal Lago, Giulio Guerrieri, Damiano Mazza, and Claudio Sacerdoti Coen.