Re: tail recursion

[halstead@crl.dec.com]

So far I think Jinx has the best handle on a reasonable definition of
the tail-recursion requirement in Scheme (whether or not we consider the
requirement to be a matter of "semantics").  Every physical machine
has finite resources (whether or not it is easy to view any of those
resources as "memory" in any traditional sense).  So the way I would
apply Jinx's criterion would be to say that a Scheme implementation M
on some machine is properly tail-recursive if it can run every program
that runs successfully on the reference implementation M0 when M0 is
constrained to have only some (nontrivial?) quantity Q0 of memory.

Even a data-flow machine will run out of some resource (e.g., token
storage) if tries to keep too much data around, so I think this definition
applies just fine to data-flow machines.

One may argue whether this definition is a matter of "semantics," but I'd
certainly defend the definition as meaningful and relevant.  On the other
hand, I'd hate to be the poor schmuck who's stuck with the job of proving
that some moderately complex, real-world implementation really satisfies
this criterion.

To the people who don't like this definition:  what is there in it that
is either fuzzy or contrary to the intuitive or desirable specification
of Scheme's policy on tail calls?  In what ways is the definition too
restrictive, or not restrictive enough?

To the people who do like it:  I'm curious whether this definition
could ever be used as anything more than a debating device.  Has
anybody tried to demonstrate the correctness of an implementation's
handling of tail calls using the level of rigor suggested by this
definition?						-Bert