[r6rs-discuss] [Formal] Allow compilers to reject obvious
bear at sonic.net
Wed Feb 28 14:22:00 EST 2007
On Sat, 24 Feb 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?
For my $.02, no it should not. Nontermination is a result
distinct from the empty list; to assume one just because the
other is considered to be an error is to lie. IOW, if the
logic of the code dictates a nonterminating process, then
the nontermination *IS* the correct result of running it.
More information about the r6rs-discuss