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.
>
> -t
>
>
>
--
~jrm
Received on Sun Feb 25 2007 - 00:35:13 UTC