And, to give a friendly noogie to Cowan -- if I can't recognize
Shannon's conceptions in the spec for ports, I'm far less interested
in R6RS. Unicode is great, but not divine.
Yes, that's right, I've deliberately been a bit silly here, regards,
-t
Thomas Lord wrote:
Joe Marshall wrote:
I was probably too vague, too. Let me try again.
Suppose we have this procedure:
(define (collatz x)
(cond ((<= x 1) '())
((even? x) (collatz (/ x 2)))
(else (collatz (+ (* x 3) 1)))))
and we use it thus:
(define (foo x)
(cons 'foo (collatz x)))
The compiler cannot prove that collatz terminates, yet it can
prove that *if* it terminates it returns the empty list. Thus
(foo x) can only return the list (foo). Should the compiler be
allowed to assume this?
Doesn't it rather depend on your constructions in the semantics?
Should R6RS answer that question? Probably not.
Should R6RS allow an implementation, if it can prove that a
continuation of a call to (foo) is strict only in a "reasonably
constructive" account of meaning, allow a terminating interpretaion?
Perhaps.
ONAG! (Maritn-Lof, Scott, etc) Kids need to get through
naive set theory to category and foundations..... And, hey,
it's also a good fit for qualitative analysis of computer
architectures...
Regards,
-t
On 2/24/07, Thomas Lord <[EMAIL PROTECTED]> wrote:
Joe Marshall wrote:
>
> I don't think I missed your point, but I think you didn't say what
> you wanted.
That's my stronger intuition, too. It's freakin' hard to say exactly
what I mean especially since, in some important areas, I haven't
had time to personally do or check certain math.
> I happen to think it would be fine for a compiler to
> ignore non-termination when compiling.
>
Which, while trivially true, if you get me, is roughly
a non-sequitor.
-t
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
