Why is there a space leak here?

[Jörgen Gustavsson]

Tom Moertel wrote:

> Okay, then, what is the *right* way to reason about these things?

I will take the oppurtunity to advertise some recent work I have been
doing together with David Sands.

I think that the call-by-need lambda calculus is a very good starting
point for gaining intuition about call-by-need beacuse it gives a way to
reason about call-by-need computation at the term level. But the
call-by-need lambda calculus was not designed for reasoning about space -
there are  terms which are considered equivalent which when you replace
one by the other in a whole program may change the asymptotic space
behaviour of the program. Therefore, we have been working on a theory of
space equivalence based on an operational semantics for a small subset of
Haskell. We have used the theory to reason about the to different
definitions of the function any that were discussed on the list some
months ago and I think it could be used in this case too. If you are
interested you can find a draft paper at www.cs.chalmers.se/~gustavss/.
We will submit the final version to ICFP in a few weeks so we would be
very grateful for any comments.

Regards,
   Jörgen Gustavsson.