I changed the topic because this particular point has very little
to do with Will's original question. I'd abandon the thread altogether,
but I find this topic to be amusing to me.
On 2/28/07, bear <bear_at_sonic.net> wrote:
>
>
> 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.
Nontermination isn't a result in the standard sense.
In
_at_inproceedings{ rozas92taming,
author = "Guillermo Juan Rozas",
title = "Taming the Y Operator",
booktitle = "{LISP} and Functional Programming",
pages = "226-234",
year = "1992",
url = "citeseer.ist.psu.edu/169695.html" }
Rozas argues in section 6 that such an optimization is defensible because it
is not possible to write a program that can detect the difference (that is, a
program that will return 1 given the optimized version and 2 given the
non-optimized
version). He suggests that disabling cases like the above which may be
controversial would also disable the same optimization for
non-controversial cases.
I agree for these reasons:
1. It is impossible to prove termination in the general case, and very hard
even in the commonly encountered case.
2. If you require exactly the same termination in optimized versus
unoptimized code, then you'd have to be sure that each clause
that could diverge be executed in the same order in the optimized code.
3. This would disable all sorts of useful and standard optimizations like
common subexpression elimination, loop unrolling, lambda lifting,
and even constant folding! (consider my collatz program above and
change it to return a number. Now consider the expression (* 0
(collatz x))
Clearly this *has* to be zero if it is anything, but if we require it to
preserve nontermination, we cannot optimize it.)
--
~jrm
Received on Wed Feb 28 2007 - 15:19:29 UTC