TY - GEN
T1 - Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
AU - Accattoli, Beniamino
AU - Belo Lourenço, Cláudio
AU - Ghica, Dan R.
AU - Guerrieri, Giulio
AU - Sacerdoti Coen, Claudio
N1 - Publisher Copyright:
© 2025 Copyright held by the owner/author(s).
PY - 2025/12/13
Y1 - 2025/12/13
N2 - 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. We study the relationship between the two approaches. We adopt a simple λ -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 (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. 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.
AB - 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. We study the relationship between the two approaches. We adopt a simple λ -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 (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. 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.
KW - Lambda calculus
KW - abstract machine
KW - program transformation
UR - https://www.scopus.com/pages/publications/105025398543
U2 - 10.1145/3756907.3756922
DO - 10.1145/3756907.3756922
M3 - Conference contribution
AN - SCOPUS:105025398543
T3 - Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming, PPDP 2025, Co-located with the 41st International Conference on Logic Programming
BT - Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming, PPDP 2025, Co-located with the 41st International Conference on Logic Programming
A2 - Biernacka, Malgorzata
A2 - Olarte, Carlos
A2 - Ricca, Francesco
A2 - Cheney, James
PB - Association for Computing Machinery, Inc
T2 - 27th International Symposium on Principles and Practice of Declarative Programming, PPDP 2025
Y2 - 10 September 2025 through 11 September 2025
ER -