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.