[r6rs-discuss] [Formal] Allow compilers to reject obvious
jmarshall at alum.mit.edu
Sun Feb 25 00:35:13 EST 2007
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?
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.
More information about the r6rs-discuss