Possibilities and Limitations of Call-by-Need Space Improvement

Jörgen Gustavsson and David Sands

To appear at International Conference on Functional Programming (ICFP01), Firenze, Italy, 3-5 September 2001


Innocent-looking program transformations can easily change the space complexity of lazy functional programs. The theory of \emph{space improvemement} seeks to characterise those local program transformations which are guaranteed never to worsen asymptotic space complexity of any program. Previous work by the authors introduced the space improvement relation and showed that a number of simple local transformation laws are indeed space improvements. This paper seeks an answer to the following questions: is the improvement relation inhabited by interesting program transformations, and, if so, how might they be established? We show that the asymptotic space improvement relation is semantically badly behaved, but that the theory of \emph{strong space improvement} posesses a fixed-point induction theorem which permits the derivation of improvement properties for recursive definitions. With the help of this tool we explore the landscape of space improvement by considering a range of classical program transformations.

Server START Conference Manager
Update Time 11 May 2001 at 15:31:50
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems