I am posting this as an individual member of the Scheme community. I am not speaking for the R6RS editors, and this message should not be confused with the editors' eventual formal response.
Matthias Felleisen wrote: > You keep evading my real question. So can you produce an algorithmic > description of when you will allow compilers to give up? I could, but I quite purposefully did not and will not. If I did, it would probably take the form of a complete proof procedure for some logic that incorporates a formal semantics such as the one in the draft R6RS, and any such thing would be partly arbitrary, inasmuch as it could be replaced by a stronger system. (For those of you who are still following along at home, that's a corollary of one of Goedel's incompleteness theorems.) A formal statement of that kind of algorithm would not be very enlightening; the paragraph I suggested in my formal comment says it better. The important thing is the word "allow". I do not wish to require any compiler to implement a complete proof procedure for the predicate described in my formal comment, and I certainly do not wish to require any compiler to decide how such attempted proofs will come out, since that is recursively undecidable. Some have argued, quite reasonably, that the criterion for rejecting a program should be the same in every implementation. Reasonable though it be, that seems a little odd to me, since the result of macro expanding (let alone executing) a program will differ between implementations, with some programs blowing up at macro expansion time (or run time) in some implementations but not others, while some will blow up some but not all of the time in yet others. I do understand the sentiment, however whimsical it may seem to me. If we accept that the criterion for rejecting a program should be the same in all implementations, then the criteria should be decidable. In my opinion, criteria that are supposed to be the same in all implementations should also be simple; otherwise it is hard to reason about the criteria, which seems like the main benefit we could hope to achieve by requiring the criteria to be the same. (I am discounting portability somewhat, because absolute portability is a lost cause in the presence of low-level macros.) As at least one person has argued, the implementation-independent criteria for rejection that are laid down in the draft R6RS might already be too complicated. Will _______________________________________________ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
