Space Improvements and Equivalences in a Functional Core Language

TL;DR

This paper investigates space improvements in a polymorphic call-by-need functional language, providing formal results on transformations that optimize or preserve space usage, including bounds and classifications of transformations.

Contribution

It introduces a relaxed space measure, proves space improvement properties for most reduction rules, and classifies transformations as space-leaks or safe, advancing understanding of space behavior in functional language optimizations.

Findings

Most reduction rules are space improvements

Translation into machine expressions is a space equivalence

Certain transformations are classified as space-leaks or safe

Abstract

We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences, all but one reduction rule of the calculus are shown to be space improvements, and for the exceptional one we show bounds on the space increase. Several further program transformations are shown to be space improvements or space equivalences in particular the translation into machine expressions is a space equivalence. We also classify certain space-worsening transformations as space-leaks or as space-safe. These results are a step forward in making predictions about the change in runtime space behavior of optimizing transformations in call-by-need functional languages.