Re: RA with MV attributes
Date: 18 Jan 2007 14:19:27 -0800
Message-ID: <1169158767.702409.237830_at_v45g2000cwv.googlegroups.com>
On Jan 18, 10:13 am, Gene Wirchenko <g..._at_ocis.net> wrote:
>
> If you can not tell if said program will ever terminate, it will
> not be possible, in general, to tell if it will ever generate an
> integer overflow.
I don't think this is correct. At least, I am pretty sure that it is possible to generate a proof of overflow-freedom without a proof of termination. However you said "in general" and, as you pointed out earlier in so many words , it is not possible to decide any of these qualities *in general.* In fact, if I understand Rice's theorem, *all* nontrivial properties of code are undecidable. This is far from meaning that termination analysis is valueless, however; on the contrary.
Note that there are many useful systems in which it is not possible to express algorithms that do not halt. These systems are of course not Turing complete, but that doesn't mean they are not useful. If I am not mistaken propositional calculus is decidable. Note also that join, union, project, etc. all have the property of always terminating when applied to finite relations.
Marshall Received on Thu Jan 18 2007 - 23:19:27 CET