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

From: Thomas Lord <lord>
Date: Wed Feb 28 15:01:01 2007

bear wrote:
> 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.
>
>


What about computations that are non-terminating under, say,
a reference operational semantics for portable programs
but that a compiler can prove converge on some value?
What if the value they converge is transfinite, in some way,
but the surrounding computation is ultimately strict in only some
finite set of bits?


(define (naturals)
  (let loop ((x 0)) (cons x (loop (+ 1 x)))))

(display (car (naturals)))


I wouldn't expect a program like that to have a portable
interpretation but it would be odd to forbid it of implementations
unless we prove some necessary contradiction with a
reasonable set of portable guarantees about more normal
programs.

You could take that further. For example, if an implementation
permits certain exotic numbers, you might have two expressions
which don't portably terminate and which, in an extended semantics
yield transfinite numbers from which we can't extract any
bits even though we can compute a relative order between the
two numbers -- so computations strict in the types and relative
order of the results of those expressions might still reasonably
run in finite time.

I admit its weird to think about implementations with these
properties but they don't strike me as something R6 ought to
rule out.

If you accept that as a possibility, then it is a mistake for the
standard to require that any procedure is total and effective
over the domain of any of the fundamental types.


-t






> Bear
>
>
Received on Wed Feb 28 2007 - 15:09:30 UTC