Re: Transparent space requirements (was Re: tail recursion proposal)

[William D Clinger <will@ccs.neu.edu>]

Stephen Adams wrote:
> My vested interest aside, how difficult is it to make space
> requirements transparent?  Has anyone a proposal?

I have written a paper on this, and have submitted it to a
conference.  It is more tedious than difficult, but it does
require a great deal of care to allow for the following:

    1.  The wide variety of ways in which an implementation
        can leak space, yet continue to be regarded as a
        reasonable and conforming implementation.
    2.  The partially unspecified semantics of many language
        constructs and standard procedures, especially those
        that perform inexact arithmetic.

> A space requirement would have to have some concept of live
> data.  I would advise against anything like the `safe for
> space complexity' idea that is thriving in the ML community.

Scheme's requirement for proper tail recursion is itself a
kind of "safe for space complexity" property.  I have
formalized 13 others, including the one due to Andrew Appel
that is popular within the SML community.  For the 14 notions
that I have formalized, Appel's notion is minimal but not
least.

Will