Closure Conversion, Flat Environments, and the Complexity of Abstract Machines

TL;DR

This paper explores the relationship between closure conversion and abstract machines, introducing a new proof technique, a novel environment handling method, and analyzing the impact on time complexity in functional language compilation.

Contribution

It presents a simple proof technique for closure conversion correctness, a new environment handling approach in abstract machines, and an analysis of complexity changes due to closure conversion.

Findings

Closure conversion reduces dynamic costs in abstract machines.

Closure conversion increases initial code size.

Overall machine complexity remains unchanged after conversion.

Abstract

Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building closures pairing the transformed functions with the environment of their free variables. Abstract machines rely on similar and yet different concepts of closures and environments. In this paper, we study the relationship between the two approaches. We adopt a very simple {\lambda}-calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion. Moreover, we focus on the simple case of flat closures/environments, that is, with no sharing of environments. We provide three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not suffering the shortcomings of other styles. Thirdly, we study the machines from the point of view of time complexity, adapting analyses by Accattoli and co-authors. We show that closure conversion decreases various dynamic costs while increasing the size of the initial code. Despite these changes, the overall complexity of the machines before and after closure conversion turns out to be the same.