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

From: Thomas Lord <lord>
Date: Sun Feb 25 00:51:06 2007

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 <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:59:30 UTC