[r6rs-discuss] [OT] Should compilers preserve termination?

From: <bear>
Date: Thu Mar 8 20:00:19 2007

After reading all the comments about preservation of
nonterminating behavior, I think I see things from
a different perspective than I started with, and I've
reached a conclusion that's more broadly applicable
than just nontermination.

My initial response was that the code should do exactly
what it says it does - and if it describes a nonterminating
process, then the process should not terminate, because
people might conclude incorrect things (like a mathematical
termination property, which they'll never ever be able to
prove) from the termination of that code.

But the other camp says that "we presume that the code is
error-free; if the only non-error result is known in
advance, we may optimize the process by eliding the
computation."

Now, on its face, this implies that "it is an error" to
create code describing a nonterminating process, and that
the implementation may handle errors however it wants.
It's analagous to code that accepts a programmer declaration
for a type that the compiler cannot infer; if the programmer
is wrong, the results of the computation are undefined
because a bit pattern with no typetag will be misinterpreted.
In this case, the (implicit) declaration is that the code
terminates; we make a strong assumption, and if we are wrong
in that assumption, then we get a result where otherwise
we would get a nonterminating process.

But requiring a compiler mode that "reports all errors"
is most clearly impossible in this case, for reasons that
should become clear if you think about it forever.

And as I think about it, the idea that someone might
erroneously conclude that a mathematical termination
property exists (without proving it) is pernicious in
itself. No rigorous proof of the termination property
can be had in this circumstance, and no one whose opinion
is supposed to *matter* should ever fall into the trap of
testing something in a few cases and then assuming a
universal law. All that a thousand trials in code will give
you is an idea that in *practice* nonterminating cases
are rare. And if the system simply *defines* nontermination-
or-single-result cases as having the single result, this
"practical termination property" is true anyway.

I think we come down to this point, and my final recommendation
on the matter - which is more broadly applicable than just talking
about nontermination itself. The standard needs to say explicitly
that if an implementation can prove that there is only one possible
return value from an error-free execution of some code, then
it may elide the execution of the code and return that value.

"error-free" in this context needs to be defined rigorously though;
nontermination is the only error I can think of right now that is
neither statically provable, nor reliably detectable at runtime.
For that reason, nontermination *is* such a critical error. I
cannot think of others, but if there are any, they should be handled
the same way.

                                Bear
Received on Thu Mar 08 2007 - 20:00:04 UTC