[r6rs-discuss] [Formal] Allow compilers to reject obvious violations

From: Thomas Lord <lord>
Date: Sun Feb 25 00:46:35 2007

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 <lord_at_emf.net> 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
>>
>>
>>
>
>
Received on Sun Feb 25 2007 - 00:55:02 UTC