Space Improvements and Equivalences in a Functional Core Language

Manfred Schmidt-Schauß
(Goethe-University Frankfurt am Main)
Nils Dallmeyer
(Goethe-University Frankfurt am Main)

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.

In Horatiu Cirstea and David Sabel: Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), Oxford, UK, 8th September 2017, Electronic Proceedings in Theoretical Computer Science 265, pp. 98–112.
Published: 16th February 2018.

ArXived at: https://dx.doi.org/10.4204/EPTCS.265.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org